Formal Analysis of Hybrid-Dynamic Timing Behaviors in Cyber-Physical Systems

Autor:	Huang, Li, Kang, Eun-Young
Rok vydání:	2019
Předmět:	Computer Science - Software Engineering
Druh dokumentu:	Working Paper
Popis:	Ensuring correctness of timed behaviors in cyber-physical systems (CPS) using closed-loop verification is challenging due to the hybrid dynamics in both systems and environments. Simulink and Stateflow are tools for model-based design that support a variety of mechanisms for modeling and analyzing hybrid dynamics of real-time embedded systems. In this paper, we present an SMT-based approach for formal analysis of the hybrid-dynamic timing behaviors of CPS modeled in Simulink blocks and Stateflow states (S/S). The hierarchically interconnected S/S are flattened and translated into the input language of SMT solver for formal verification. A translation algorithm is provided to facilitate the translation. Formal verification of timing constraints against the S/S models is reduced to the validity checking of the resulting SMT encodings. The applicability of our approach is demonstrated on an unmanned surface vessel case study. Comment: 4 pages, accepted as a work-in-progress paper in RTSS-BP2019
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1910.14306 Zobrazit plný text záznamu View this record from Arxiv