Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow

The efficient design of safety-critical cyber-physical systems ( CPS) requires the co-modeling and -verification of its physics, architecture and functionalities. Existing co-modeling formalisms do not account for these three design aspects into account uniformly. AADL is a precise formalism for modeling architecture and prototyping real-time hardware platforms, but it delegates co-modeling physical and software behaviors to so-called annexes. By contrast, Simulink/Stateflow (S/S) is strong for modeling interacting physical and software behaviors, but weak for modeling architecture and hardware platforms. To address this issue, this paper considers the combination of AADL and S/S to co-model CPSs and presents a method to uniformly analyze and verify this combination. AADL circle plus S/Sprovides a unified graphical co-modeling environment for CPS design and supports simulation through C code generation. We present a formal semantics of AADL circle plus S/Sby translating it to Hybrid Communicating Sequential Processes (HCSP), which yields a deductive verification framework for AADL circle plus S/Smodels based on Hybrid Hoare Logic (HHL). We also prove the correctness of the translation of AADL circle plus S/Sto HCSP. The effectiveness of our approach is illustrated by the realistically-scaled case study of an automatic cruise control system. (C) 2021 Elsevier B.V. All rights reserved.