模型驱动形式设计与验证

针对航天、高铁、军工等领域安全攸关嵌入式系统的设计挑战，探讨基于形式化方法的建模、验证与代码生成等核心理论和技术。本报告聚焦模型驱动的安全攸关嵌入式系统形式设计，涉及(1)基于Simulink/Stateflow和混成CSP的嵌入式系统复杂行为层次建模方法，具备图形建模的易用性和形式模型的严格性；(2)混成Hoare逻辑理论和验证系统，支持连续动态与时序性质的形式化规约与验证；(3)不同层次模型之间的转换算法，包括从已验证的形式模型到代码的自动转换，保证代码生成的可靠性；(4)基于信号时序逻辑的系统运行时监测分析方法。旨在提供安全攸关嵌入式系统形式设计和分析的全方位视角。

安杰，中国科学院软件研究所副研究员、博士生导师。主持国家级青年人才项目、中国科学院率先行动引才计划项目等。长期从事软件形式化方法研究，聚焦安全攸关系统形式设计与验证理论前沿，在信息物理融合系统形式建模、验证与分析方面取得了若干突破，相关成果在国家深空探测工程中得到应用。近几年在CAV、FM、EMSOFT等形式化方法和嵌入式系统领域权威国际期刊或会议上发表论文四十余篇，获FMAC 2019、ATVA 2025最佳论文。