Mars 2.0：一款用于信息物理系统建模、分析、验证与代码生成的工具链
Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems
AI总结：
本研究推出信息物理系统设计工具链Mars 2.0，整合AADL与Simulink/Stateflow建模，通过经形式化证明的转换流程实现HCSP建模、验证及SystemC/C代码自动生成，支持安全关键系统的模型驱动设计。
摘要：
我们推出用于信息物理系统建模、分析、验证与代码生成的Mars 2.0。Mars 2.0在Mars 1.0的基础上整合了多项重要扩展与改进，支持结合AADL（架构分析与设计语言）与Simulink/Stateflow进行信息物理系统设计，为待开发系统的功能、物理特性与架构建模提供了统一的图形化框架。对于安全关键系统，其AADL与Simulink/Stateflow组合模型可通过以下步骤开展形式化分析与验证：首先，工具链自动将AADL和Simulink/Stateflow模型转换为Hybrid CSP（HCSP，即混合通信顺序进程，是CSP用于混合系统形式化建模的扩展）；其次，可通过HCSP模拟器对HCSP进程进行仿真，为弥补仿真的不完备性，还可借助Isabelle/HOL中的Hybrid Hoare Logic证明器以及自动化程度更高的HHLPy证明器对其进行验证；最后，可从经过验证的HCSP进程自动生成SystemC或C语言实现。从AADL与Simulink/Stateflow到HCSP的转换、以及从HCSP到SystemC或C的转换，均通过形式化证明保证正确性。该方法支持基于图形化与形式化模型、以及经证明正确的转换流程，开展安全关键信息物理系统的模型驱动设计。我们在多个不同复杂度的基准测试用例（包括若干工业规模的实例）上演示了该工具链的使用。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
