Unified Graphical Co-modelling, Analysis and Verification of Cyber-physical Systems by Combining AADL and Simulink/Stateflow

The design of safety-critical cyber-physical systems (CPSs) involve several dimensions, including physics, hardware rchitecture and software functionality. It is desirable to design CPSs by taking these issues into account uniformly and yet, few existing design workflows support this aim. For instance, AADL is an architecturecentric modelling formalism for CPSs, which focuses on modelling architecture and prototyping real-time hardware platforms, but it delegates physical and software behavioral models to so-called annexes. By contrast, Simulink/Stateflow (S/S) focuses on modelling interacting physical and software behaviors, but does not render the non-functional characteristics of their hardware platforms. To address this issue, in [1], we proposed the combination of AADL and S/S, called AADL S/S, to comodel CPSs and presented a method to uniformly analyse and verify them. AADL S/S provides a unified graphical co-modelling environment for CPS design and supports simulation through C code generation. Also, [1] presented a formal semantics of AADL S/S by translation to Hybrid Communicating Sequential Processes (HCSP), yielding a deductive verification framework of the combined models using Hybrid Hoare Logic (HHL). Additionally, [1] proved the correctness of the translation of AADL S/S to HCSP.