奖项：2019年度上海市科技进步奖特等奖
项目名称：面向重大工业装备核心控制软件的安全可信保障技术及应用
万物互联的时代正在到来，电力运行、轨道交通、航空航天、大型装备……越来越多关系国计民生的大型系统都要靠复杂而智能的软件系统运行。如果这些软件“带病”上岗，一旦“发病”或被人操控，后果将不堪设想。
早在十多年前，为了给国产软件打上学术界、产业界都认可的“安全可信”标签，中国科学院院士、华东师范大学软件学院教授何积丰带领团队从基础理论入手，破解重重难题，自主研发出了国内首款通过国际权威认证的测试工具SmartUnit，并形成11款具有完全自主知识产权的形式化建模、测试与验证工具，其中6款已商业化，近三年销售额达1.5亿元。
目前，这一系列工具已为我国风云四号卫星、探月工程三期等航空航天重大任务提供了支撑，并为上海地铁10号线、17号线等多条国内外轨道交通线路提供安全保障。
破解软件“信任危机”，解决产业“卡脖子”难题
“十几年前我们就意识到，软件不总是可以让人信任的。”何积丰回忆，当时不断有企业找上门来：有的引进了国外软件，却发现它水土不服，但又如同“黑匣子”，难以优化；有的自主开发软件产品，却不知如何说服客户信任它……
归根到底，我国要建立一套软件“体检”系统，通过它实现对软件的自动化验证、测试，及时找出软件中存在的隐患，确保运行安全无虞。何积丰说，随着软件运行和开发环境从传统的封闭、静态，转向开放、动态、多变的互联网环境，“可信软件”必将成为现代软件技术发展和应用的重要趋势和必然选择。
2007年底，国家自然科学基金委启动了“可信软件基础研究”重大研究计划，何积丰带领团队投入到艰苦的研发中。
软件的复杂性“分析难”、正确性“验证难”、可靠性“保障难”如同三座大山，矗立在科研团队面前。运用深厚的数学功底，何积丰决定从基本理论与算法入手，解决科学问题，建立方法体系，从而破解国产软件的“信任危机”。
“这是一个漫长的螺旋式上升的过程。我们从产业需求中发现问题，再回到产业中去验证，不断发现新问题。”十几年来，他们发展起了控制软件的可信保障技术，开发出了一系列自主可控的软件全生命周期工具链。值得一提的是，团队所开发的软件工具能对软件在数学层面进行仿真和验证，在代码生成之前就发现其中的缺陷，提醒开发者及时改进。
聚焦安全攸关领域，中国企业与国际同行同台竞技
伴随安全可信软件保障技术的诞生与发展，国内相关软件企业开始在国内外市场崭露头角。
上海创景信息科技有限公司是可信软件项目团队中唯一一家民营企业，公司从代理国外软件产品起步，逐步转向自主开发软件工具产品，可理论缺乏令研发之路荆棘丛生。2013年，公司与华师大成立联合实验室，将何积丰团队的理论成果转化到工具中。过去数年，这些工具成功支撑了神舟八号与天宫一号对接、风云四号卫星研制等多项重大航天任务。
▲可信软件项目应用于卡斯柯信号有限公司无人驾驶工程中心
身为项目团队成员，为上海地铁提供软件运维服务的卡斯柯信号有限公司，十年前开始投入自主运行系统研制。2012年，公司与何积丰团队开启全面合作，如今已成功实现了上海地铁17号线列车运行控制系统的100%自主研发。由该公司自主研发的城市轨道交通信号解决方案成功部署于埃塞俄比亚斯亚贝巴轻轨，成为中国第一套“走出去”的自主信号系统解决方案，开始与国际企业同台竞技。
据统计，可信软件项目新增直接经济效益和利润累计超过14.2亿元，实现利润超2.1亿元，间接带动了千亿产值的产业效益。
2018年，依托该项目，作为支撑上海科创中心“四梁八柱”的重要创新力量，上海工业控制系统安全创新功能型平台成立。聚焦轨道交通、航空航天、汽车电子和电力控制等安全攸关领域的软件研制，未来平台孕育的创新成果将辐射长三角，带动相关产业发展。