项目属于“计算机科学与技术”领域。控制软件是重大工业装备的核心中枢，此类软件出现问题会造成灾难性的后果，例如近期的两起波音737 MAX8客机坠毁事件。如何保障控制软件的安全可信是国际公认的重大挑战，也是我国经济转型升级亟需解决的“卡脖子”问题。在国家基金委“可信软件基础研究”重大研究计划等项目资助下，项目牵头单位聚焦软件安全可信保障技术，历经十余年研究并与企业协同创新，攻克了软件安全可信保障技术的三大难题，即正确性“验证难”、可靠性“保障难”与复杂性“分析难”。项目组采用形式化分析、测试与验证等核心技术，实现了覆盖软件全生命周期的开发与验证工具链，有力保障了重大工业装备核心控制软件研制的安全可信。项目技术创新如下：1、首创了形式化统一建模理论与多维度验证技术：针对由两位图灵奖得主提出的并发模型CCS与CSP是否互洽的开放问题，建立了并发程序的统一模型框架，解决了困扰国际学术界二十余年的难题。基于该理论提出的多维度验证技术支持软件系统的精确描述与严格验证，解决了大规模复杂需求形式化建模与一致性验证的难题。微软首席科学家Bjorner评价部分成果是“关联CCS与CSP迹语义的奠基性结果”。成果应用于风云四号气象卫星、嫦娥三期再入返回飞行器等系统的核心软件研制过程。2、构建了面向信物融合的多层次仿真与测试技术：面向轨道交通等典型信息物理融合系统测试效率低等问题，构建了多层次仿真与测试技术，有效提升了控制系统的测试效率与质量。该技术将卡斯柯公司(国内排名第一)地铁信号系统的集成测试周期从1个月缩短为1周，支撑其成为国内首个获国际最高安全认证SIL4的信号系统。该技术为中国商飞、航天八院等单位关键软件产品研制提供保障。3、发明了不确定环境下多属性量化评估与分析技术：针对控制系统实时性等关键属性，首次建立了不确定环境下软件多属性定量评估、实时度量、失效估算等综合量化分析技术，解决了软件复杂性精确定量分析的难题，IEEE院士Yakovlev教授评价其“性能定量评估技术优于传统方法”。成果应用于国内首条无人驾驶线路(上海10号线)、“天宫一号与神舟八号对接任务”等重大任务。4、实现了支撑软件全生命周期的开发与验证工具链：面向行业缺乏“高效可用”和“自主可控”的软件开发与验证环境，自主研发了支撑软件全生命周期的工具链，填补多项技术空白，已替代部分国外同类产品并在若干关键技术环节形成超越，近三年工具销售额达1.5亿。项目授权发明专利27项，获得软著62项，制定行业标准2项，出版英文专著1本，发表高水平论文60篇；获6项省部级以上奖励；近三年新增销售额14.2亿元，新增利润2.1亿元。项目第一完成人担任基金委重大研究计划“可信软件基础研究”首席科学家，支持全国科研院所项目107项，有效提升了我国可信软件研究的国际竞争力，极大推动了软件可信技术在工业界的转化与应用。