安全攸关嵌入式系统设计和形式验证关键技术

1. 成果简介

我们围绕安全攸关软件理论、技术与应用开展研究，重点关注国家重大需求领域，例如航天飞行器、飞机、高铁等，旨在构建安全可靠的信息物理融合系统。我们开发了基于模型驱动的嵌入式系统建模、分析、验证与代码生成工具链MARS。该工具链采用AADL和Simulink/Stateflow进行图形建模，便于工程师使用，并支持自动仿真。我们实现了从图形模型到HCSP形式模型的自动转换，支持形式验证，确保系统的严格正确性。此外，我们还实现了从形式模型到SystemC或C代码的自动生成，保证了转换的正确性，从而生成完全可靠的代码。目前，MARS已成功应用于航天控制软件、高铁控制系统和高速飞车交接控制系统等实际案例的形式验证中。

2. 技术创新点

该成果为基于形式验证的嵌入式系统设计理论和工具。

3. 技术成熟度

该成果当前处于小试阶段（实验室验证）。

4. 可应用领域

该成果可应用于航天、航空、高铁等安全攸关领域嵌入式系统的可靠设计和形式验证中。

5. 联系人

王淑灵，wangsl@ios.ac.cn，18612791263