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

Full Citation in the ACM Digital Library

SESSION: Papers

ObjSim: efficient testing of cyber-physical systems

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.

Formal verification of discrete event model

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.