We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improvements, allowing the design of cyber-physical systems using the combination of AADL and Simulink/Stateflow, which provide a unified graphical framework for modeling the functionality, physicality and architecture of the system to be developed. For a safety-critical system, formal analysis and verification of its combined AADL and Simulink/Stateflow model can be conducted via the following steps. First, the toolchain automatically translates AADL and Simulink/Stateflow models into Hybrid CSP (HCSP), an extension of CSP for formally modeling hybrid systems. Second, the HCSP processes can be simulated using the HCSP simulator, and to complement incomplete simulation, they can be verified using the Hybrid Hoare Logic prover in Isabelle/HOL, as well as the more automated HHLPy prover. Finally, implementations in SystemC or C can be automatically generated from the verified HCSP processes. The transformation from AADL and Simulink/Stateflow to HCSP, and the one from HCSP to SystemC or C, are both guaranteed to be correct with formal proofs. This approach allows model-driven design of safety-critical cyber-physical systems based on graphical and formal models and proven-correct translation procedures. We demonstrate the use of the toolchain on several benchmarks of varying complexity, including several industrial-sized examples.

翻译：本文介绍用于信息物理系统建模、分析、验证与代码生成的Mars 2.0工具。Mars 2.0集成了Mars 1.0的多项重要扩展与改进，支持通过AADL与Simulink/Stateflow的联合设计，为待开发系统的功能、物理特性及架构建模提供统一的图形化框架。针对安全关键系统，可通过以下步骤对其联合AADL与Simulink/Stateflow模型进行形式化分析与验证：首先，工具链自动将AADL与Simulink/Stateflow模型转换为混合CSP（Hybrid CSP，HCSP），即CSP为形式化建模混合系统的扩展；其次，利用HCSP模拟器对HCSP进程进行仿真，并通过Isabelle/HOL中的混合霍尔逻辑证明器及更自动化的HHLPy证明器对仿真不完备性进行补充验证；最后，根据验证后的HCSP进程自动生成SystemC或C语言实现。从AADL与Simulink/Stateflow到HCSP的转换，以及从HCSP到SystemC或C的转换均通过形式化证明保证正确性。该方法基于图形化与形式化模型以及经证明正确的转换流程，实现安全关键信息物理系统的模型驱动设计。我们通过多个不同复杂度的基准测试（包括若干工业规模实例）展示了该工具链的应用效果。