Research Article
An Semi-formal Co-verification Approach for High-Assurance CPS
@INPROCEEDINGS{10.1007/978-3-030-32216-8_16, author={Yu Zhang and Mengxing Huang and Wenlong Feng}, title={An Semi-formal Co-verification Approach for High-Assurance CPS}, proceedings={Simulation Tools and Techniques. 11th International Conference, SIMUtools 2019, Chengdu, China, July 8--10, 2019, Proceedings}, proceedings_a={SIMUTOOLS}, year={2019}, month={10}, keywords={Cyber-Physical Systems Semi-formal Co-simulation}, doi={10.1007/978-3-030-32216-8_16} }- Yu Zhang
Mengxing Huang
Wenlong Feng
Year: 2019
An Semi-formal Co-verification Approach for High-Assurance CPS
SIMUTOOLS
Springer
DOI: 10.1007/978-3-030-32216-8_16
Abstract
Cyber-Physical Systems (CPS) are often mission-critical, therefore, they must be high-assurance. High-assurance CPS require extensive formal verification. Formal verification techniques can discover subtle design errors where simulation fails. However, due to the state explosion problem, formal techniques usually cannot handle large designs. This paper introduces a semi-formal verification methodology in which formal co-verification and co-simulation are tightly coupled. We propose an online-capture offline-replay approach to improve the usefulness for formal verification. We analyze these simulation traces, find some critical states and assisted with formal verification under these circumstances. The experiment results show that our approach has major potential in verifying system level properties of complex CPS, therefore improving the high-assurance of CPS.