MARS 2.0: A Toolchain for Designing Safety-Critical Cyber-Physical Systems

This paper presents MARS 2.0, an integrated toolchain for the model-driven design of safety-critical Cyber-Physical Systems (CPSs). MARS 2.0 supports an end-to-end workflow spanning unified modeling, formal verification, and trusted code generation. Building on its predecessor, MARS 2.0 introduces three key enhancements: (1) a co-modeling framework that combines AADL (for system architecture) and Simulink/Stateflow (for functional and physical behaviors)—denoted \(\textsf {AADL}\!\oplus \!\textsf {S/S} \) ; (2) provers based on Hybrid Hoare Logic (HHL) for verifying formal models; and (3) correct-by-construction code generation from verified models. In MARS 2.0, users first construct an \(\textsf {AADL}\!\oplus \!\textsf {S/S} \) model to capture the system’s architecture, control logic, and continuous dynamics in a unified framework. This model is then automatically translated into Hybrid Communicating Sequential Processes (HCSP), a formal modeling language for hybrid systems. The resulting HCSP program can be (1) simulated for rapid validation, and (2) formally verified using the HHLProver suite. Finally, once verified, the HCSP model is compiled into executable ANSI-C or SystemC code. Critically, both the “ \(\textsf {AADL}\!\oplus \!\textsf {S/S} \) to HCSP” translation and the “HCSP to ANSI-C/SystemC” code generation are backed by formal proofs of semantic preservation. By bridging industrial modeling notations with formal methods, MARS 2.0 makes rigorous CPS development accessible to engineers.