图说：可信软件技术服务轨交行业 采访对象供图
如何保障高端装备控制软件的安全可信，是国际公认的重大挑战。特别是我国航空、航天、轨道交通和电力控制等安全攸关领域，其重大装备的核心控制软件的研制技术，急需解决技术与工具产品的自主可控问题，以支撑我国经济转型升级，打破国外在该领域的垄断。由华东师范大学软件工程学院创院院长、中国科学学院院士何积丰作为第一完成人的《面向重大工业装备核心控制软件的安全可信保障技术及应用》项目，今天荣获2019年度上海市科技进步特等奖。
高可信技术是保障核心工业软件成功研制的关键手段。何积丰院士说：“控制软件是工业重大装备的中枢，是国家利器。要让它足够锋利，就需要优良的磨刀石。我们就是把铸剑的磨刀石做好做精，这样来提高重大装备核心控制软件的质量，确保它们安全可信。”项目参研单位聚焦我国重大工业装备核心控制软件的软件安全可信保障技术，对接国家“自主可控”战略部署，历经十余年深入研究，以产教学研协同创新为路径，攻克了软件安全可信保障技术的三大难题，即正确性“验证难”、可靠性“保障难”与复杂性“分析难”。
据华东师大研发人员介绍，项目组采用形式化分析、测试与验证等核心技术，首创形式化统一建模理论与多维度验证技术，解决了困扰国际学术界二十余年的难题；发明了不确定环境下多属性量化评估与分析技术，应用于载人航天工程等一批国家重要任务。项目的一大亮点是形成了系统化的自主可控软件开发工具链，覆盖了重大工业装备核心控制软件开发的全生命周期。据统计，完全知识产权的形式化建模、测试与验证工具11款，已经形成商业化产品的达6款。其中，自主研发的软件自动化测试工具SmartUnit更是成为了国内首款通过国际上公认标准TUV功能安全认证的测试工具。近三年来，仅工具销售额即达到了1.5亿。历经十余年，该项目已产生了显著的社会和经济效益。项目新增直接经济效益和利润累计超14.2亿元人民币，实现利润超2.1亿元人民币，间接带动了千亿产值的产业效益。
截至目前，该项目成果成功支撑了“风云四号”卫星发射、“神舟八号与天宫一号对接”以及“探月工程月地高速再入返回器”等在内的多项重要航天任务；项目参研单位卡斯柯信号有限公司完全自主研发的TRANAVI城市轨道交通信号系统解决方案，成功部署于东非地区的第一条城市轻轨，即埃塞俄比亚的斯亚贝巴轻轨，成为中国第一套“走出去”的自主信号系统解决方案，有力地支撑了“一带一路”倡议。
首席记者 王蔚