ISSTA 2020 Workshops
29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2020)
Powered by
Conference Publishing Consulting

4th ACM SIGSOFT International Workshop on Testing, Analysis, and Verification of Cyber-Physical Systems and Internet of Things (TAV-CPS/IoT 2020), July 19, 2020, Virtual Event, USA

TAV-CPS/IoT 2020 – Proceedings

Contents - Abstracts - Authors

4th ACM SIGSOFT International Workshop on Testing, Analysis, and Verification of Cyber-Physical Systems and Internet of Things (TAV-CPS/IoT 2020)

Frontmatter

Title Page


Welcome from the Organizers
Welcome to the Workshop on Testing, Analysis, and Verification of Cyber-Physical Systems and Internet of Things (TAV-CPS/IoT 2020) held in USA jointly with the ACM Sigsoft International Conference on Software Testing and Analysis ISSTA 2020. The workshop follows the successful editions co-located with ISSTA in 2017, ECOOP/ISSTA in 2018, and ISSTA 2019.

Papers

ObjSim: Efficient Testing of Cyber-Physical Systems
Jun Sun and Zijiang Yang
(Singapore Management University, Singapore; GuardStrike, China)
Cyber-physical systems (CPSs) play a critical role in automating public infrastructure and thus attract wide range of attacks. Assessing the effectiveness of defense mechanisms is challenging as realistic sets of attacks to test them against are not always available. In this short paper, we briefly describe smart fuzzing, an automated, machine learning guided technique for systematically producing test suites of CPS network attacks. Our approach uses predictive ma- chine learning models and meta-heuristic search algorithms to guide the fuzzing of actuators so as to drive the CPS into different unsafe physical states. The approach has been proven effective on two real-world CPS testbeds.

Publisher's Version Article Search
Formal Verification of Discrete Event Model
Zhihao Lu, Rui Wang, and Yong Guan
(Capital Normal University, China)
Ptolemy is a modeling and simulation toolkit widely used in cyber physical systems. Formal verification is a very important method to guarantee the correctness of systems. However, the proposed verification approach in Ptolemy is inconvenient and only supports a few actors. In this paper, we present a model translation based approach to verify the Ptolemy Discrete-Event model and implement a plug-in tool in Ptolemy. A set of mapping rules are designed to translate the Ptolemy Discrete-Event model into a network of timed automata. A template library that translates from actors in Ptolemy Discrete-Event model is also built in advance. A case study of traffic lights control system has been successfully translated and verified. The verification results are reliable and valid. The experimental results confirm our approach is useful to verify the Ptolemy Discrete-Event model.

Publisher's Version Article Search

proc time: 5.22