原标题：从神舟飞船对接到地铁无人驾驶……都有华东师大高可信软件自主保障！
从神舟飞船自动对接，
到上海地铁线首次实现无人驾驶，
这些天地间奇迹的背后，
正是由华东师范大学牵头的
《面向重大工业装备核心控制软件的
安全可信保障技术及应用》项目。
我国航空航天、轨道交通、
电力控制等安全攸关领域，
因为这座2019年度
上海市科技进步特等奖
而有了自主可控、
高度可信的中枢神经。
8月20日，神舟十二号乘组两名航天员聂海胜、刘伯明，成功完成第二次出舱。就在几天前，执行天舟三号货运飞船飞行任务的长征七号遥四运载火箭运抵文昌航天发射场。同时，执行神舟十三号飞行任务的载人飞船及运载火箭，正在酒泉发射场按计划同步开展各项准备工作。我国载人航天工程进入空间站阶段后，多任务交叉并行成为工作常态。
▲文昌发射场。徐瑞哲摄
今夏，深空探测方面，国家航天局探月与航天工程中心在京发放“嫦娥五号”任务的第一批月球科研样品，标志着月球样品科学研究工作正式启动。那个去月球挖土的“嫦娥五姑娘”，带着来自广寒宫的“土特产”重返地球，也被称为我国迄今最复杂的航天任务之一。
事实上，“嫦五”从月面起飞、月球轨道交会对接和地月之间再入返回等60%以上的功能，均涉及软件操控自行实现。在获得科技进步大奖的团队助力下，她才圆满完成中国无人探月“绕—落—回”三期工程的终章。
从天宫一号与神舟飞船自动对接，到上海地铁线首次实现无人驾驶，这些天地间奇迹的背后，正是由华东师范大学牵头的《面向重大工业装备核心控制软件的安全可信保障技术及应用》项目。
我国航空航天、轨道交通、电力控制等安全攸关领域，因为这座2019年度上海市科技进步特等奖而有了自主可控、高度可信的中枢神经。
工控软件不能是一个个“黑盒子”
仅空天领域，从神舟七号到风云四号，这一特等奖项目技术就在50余个航天任务中成功应用。有意思的是，华东师大软件工程学院陈仪香和蒲戈光两位教授所在团队，还依托航天五〇二所承研的“航天嵌入式软件可信性保障关键技术和应用”项目，获得了2019年度北京市科学技术进步一等奖。
嵌入式软件是航天器的重要组成部分，其可信性直接影响航天任务成败。随着我国航天事业的快速发展，嵌入式软件的数量、规模和复杂性急剧增加，其可信性保障是国内外公认的重大挑战。
几十年来，为了提高航天嵌入式软件的质量，软件工作者开展了大量的工作，取得了很好的成效。然而，动态时序、控制行为和程序实现等深层次的软件问题仍时有发生。
总体而言，现有的研制方法对人的能力、经验依赖较大；针对软件研制中的部分问题有一些解决办法，但还没有形成系统的解决方案，很难满足航天任务变化快、进度紧、质量高的需求。因此，研究系统的嵌入式软件可信性保障理论、方法、工具和环境已非常迫切。
▲支撑地铁信号系统
由此推而广之，中国装备制造业尚未足够强大，不少方面也“缺芯少魂”，这“魂”就是软件。长期以来，国内大批设备依赖舶来引进，甚至包括地铁等轨交基础设施也是以进口为主，各有各的来路。随着信息化、数字化、智能化，万物运行从独立封闭状态发展到工业互联网时代，如何确保关键领域的工控软件不是一个个“黑盒子”，没有后门也没有漏洞？
在中国科学院院士、华东师范大学软件工程学院创院院长何积丰看来，这些都构成了国家整体安全的基本支撑面，要形成一个巨大的安全保障闭环，就像绣花功夫一样急也急不来。有些情况下，软件缺陷稍纵即逝，却慢慢累积着，一个周期连到下一个周期，一个部件影响下一个部件，最终以故障形式出现。软件人和软件分析工具就要像过电影画面一样一帧帧看，让“时间切片”一步步走，确保每条代码万无一失。
攻克软件可信保障技术三大难题
十年磨一剑，磨刀石在哪？“控制软件是工业重大装备的中枢，是国家利器。要让它足够锋利，就需要优良的磨刀石。”何积丰这位软件界程序统一理论学派的开创者说，“我们就是把铸剑的磨刀石做好做精，这样来提高重大装备核心控制软件的质量，确保它们安全可信。”
记者了解到，自2008年1月起，作为上海市科技进步特等奖项目第一完成人的何积丰院士，担任国家自然科学基金委“可信软件基础研究”重大研究计划首席科学家，支持全国科研院所涉及百业的相关课题达107项，迄今整整13年过去了。
作为上海市科技功臣和教育功臣，何积丰带着整支团队冲上一线。
“我们的科学研究工作，是从产业实际出发，提炼科学问题；再通过研究成果的应用，来验证我们的想法；最终形成核心技术，去解决国家所面临的问题。”他说。而80后中，主持工作的软件工程学院年轻院长陈铭松和团队成员一起，深入行业企业打交道、“破黑盒”，以解决软件可信保障技术的三大难题。
比如，软件复杂性“分析难”：一份用户需求文件可能好几百页，同时存在网络延迟多变等运行环境的不确定性；又如，软件正确性“验证难”：以主流航空航天器百万行级别的大规模代码为例，必须让代码自动生成替代人工编写代码；再如，软件可靠性“保障难”：接受国际测评标准严、投入大、周期长，软件测试要占到开发成本一半左右。
▲获国际最高安全认证SIL4的信号系统
“如果‘闭门造车’，可能‘水土不服’。”陈铭松介绍，卡斯柯信号有限公司就是此次项目团队深入的行业企业之一，也是项目攻关的参研单位之一。2012年何积丰院士团队与卡斯柯合作至今，其产品不仅已成功部署于上海轨道交通17号线，还服务于东非地区的第一条城市轻轨——埃塞俄比亚首都亚的斯亚贝巴轻轨，后者也成为中国第一套“走出去”的自主列车运行控制系统解决方案。
历经十余年深入研究、实操实战，他们一届一届接力，攻克了三大难题，也让近千名高端软件人才从这个大项目平台出发，走向全国近百家企业，投身于轨道交通、航空航天、汽车电子和电力控制等诸多领域。
像淘宝一样上网获得共性软件服务
值得一提的是，在上海市科技进步特等奖的获奖证书上，除了第一完成单位华东师大外，其余6家都是中电科、普华等企业。可以说，一条产教学研协同创新的路径，是这项“核高基”技术成功应用的必经之途。
卡斯柯研究设计院副院长周庭梁介绍，双方依托院士专家工作站及上海轨道交通无人驾驶列控系统工程技术研究中心，针对卡斯柯自主研发的TRANAVI列车运行控制系统的核心控制软件，进行了软件形式化技术研究突破，产品满足第三方国际评估机构SIL4安全认证要求。
来自申通地铁集团技术中心的技术总监万勇兵也透露，拥有700多公里里程、400余座车站的上海轨道交通，为对接国家自主可控战略需求，聘请何积丰院士担纲首席科学家，将高可信技术应用于“智慧地铁”建设之中，助力上海保持在国内外城市轨交行业的技术领先地位和持续快速发展。
▲2018年3月，上海工业控制安全创新科技有限公司成立
不论是针对空天、汽车还是电力的中枢神经，可控可信的共性技术即通用工具，用何积丰的话比方，就是让不同行业的企业都能像淘宝一样在网上获得软件服务。从体制机制层面上，在该项目支持下，作为支撑上海科创中心“四梁八柱”的重要创新力量——上海工业控制系统安全创新功能型平台应运而生，成为上海市首批推动建设的18个研发与转化功能型平台之一。平台骨干技术团队成员，不少也是来自华东师大软件工程学院的教授，现已形成系统化的自主可控软件开发工具链，覆盖了重大工业装备核心控制软件开发的全生命周期。
数据显示，这项特等奖项目研究期间，共授权发明专利27项，获得软件著作权62项，制定行业标准2项，出版英文专著1本，发表高水平论文60篇……总体上，项目面向各行各业新增直接经济效益和利润累计超14.2亿元，间接带动了千亿产值的产业效益。
项目团队表示，未来将继续为国产大飞机、深空探测和下一代城市轨交列车运行控制系统等重大国家级技术攻关提供共性技术，形成自主可控软件人才和产业集聚效应，引领我国自主可控软件产业发展，在国际上也形成高端装备核心软件的“中国造”品牌。他们说，“给国产装备用，更要给国外设备用。”
原载｜上观新闻
文｜解放日报首席记者徐瑞哲
编辑｜吴潇岚
