TAV-CPS/IoT '20: "Formal Verification of Discrete ..."
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.
@InProceedings{TAV-CPS/IoT20p3,
author = {Zhihao Lu and Rui Wang and Yong Guan},
title = {Formal Verification of Discrete Event Model},
booktitle = {Proc.\ TAV-CPS/IoT},
publisher = {ACM},
pages = {3--4},
doi = {10.1145/3402842.3407159},
year = {2020},
}
Publisher's Version
TAV-CPS/IoT '20: "Formal Verification of Discrete ..."
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.
@InProceedings{TAV-CPS/IoT20p3,
author = {Zhihao Lu and Rui Wang and Yong Guan},
title = {Formal Verification of Discrete Event Model},
booktitle = {Proc.\ TAV-CPS/IoT},
publisher = {ACM},
pages = {3--4},
doi = {10.1145/3402842.3407159},
year = {2020},
}
Publisher's Version
TAV-CPS/IoT '20: "ObjSim: Efficient Testing ..."
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.
@InProceedings{TAV-CPS/IoT20p1,
author = {Jun Sun and Zijiang Yang},
title = {ObjSim: Efficient Testing of Cyber-Physical Systems},
booktitle = {Proc.\ TAV-CPS/IoT},
publisher = {ACM},
pages = {1--2},
doi = {10.1145/3402842.3407158},
year = {2020},
}
Publisher's Version
TAV-CPS/IoT '20: "Formal Verification of Discrete ..."
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.
@InProceedings{TAV-CPS/IoT20p3,
author = {Zhihao Lu and Rui Wang and Yong Guan},
title = {Formal Verification of Discrete Event Model},
booktitle = {Proc.\ TAV-CPS/IoT},
publisher = {ACM},
pages = {3--4},
doi = {10.1145/3402842.3407159},
year = {2020},
}
Publisher's Version
TAV-CPS/IoT '20: "ObjSim: Efficient Testing ..."
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.
@InProceedings{TAV-CPS/IoT20p1,
author = {Jun Sun and Zijiang Yang},
title = {ObjSim: Efficient Testing of Cyber-Physical Systems},
booktitle = {Proc.\ TAV-CPS/IoT},
publisher = {ACM},
pages = {1--2},
doi = {10.1145/3402842.3407158},
year = {2020},
}
Publisher's Version