8月20日，神舟十二號乘組兩名航天員聶海勝、劉伯明，成功完成第二次出艙。就在幾天前，執行天舟三號貨運飛船飛行任務的長征七號遙四運載火箭運抵文昌航天發射場。同時，執行神舟十三號飛行任務的載人飛船及運載火箭，正在酒泉發射場按計劃同步開展各項準備工作。我國載人航天工程進入空間站階段后，多任務交叉并行成為工作常態。

文昌發射場。徐瑞哲 攝

今夏，深空探測方面，國家航天局探月與航天工程中心在京發放“嫦娥五號”任務的第一批月球科研樣品，標志著月球樣品科學研究工作正式啟動。那個去月球挖土的“嫦娥五姑娘”，帶著來自廣寒宮的“土特產”重返地球，也被稱為我國迄今最復雜的航天任務之一。事實上，“嫦五”從月面起飛、月球軌道交會對接和地月之間再入返回等60%以上的功能，均涉及軟件操控自行實現。在獲得科技進步大獎的團隊助力下，她才圓滿完成中國無人探月“繞—落—回”三期工程的終章。

從天宮一號與神舟飛船自動對接，到上海地鐵線首次實現無人駕駛，這些天地間奇跡的背后，正是由華東師范大學牽頭的《面向重大工業裝備核心控制軟件的安全可信保障技術及應用》項目。我國航空航天、軌道交通、電力控制等安全攸關領域，因為這座2019年度上海市科技進步特等獎而有了自主可控、高度可信的中樞神經。

【工控軟件不能是一個個“黑盒子”】

僅空天領域，從神舟七號到風云四號，這一特等獎項目技術就在50余個航天任務中成功應用。有意思的是，華東師大軟件工程學院陳儀香和蒲戈光兩位教授所在團隊，還依托航天五〇二所承研的“航天嵌入式軟件可信性保障關鍵技術和應用”項目，獲得了2019年度北京市科學技術進步一等獎。

嵌入式軟件是航天器的重要組成部分，其可信性直接影響航天任務成敗。隨著我國航天事業的快速發展，嵌入式軟件的數量、規模和復雜性急劇增加，其可信性保障是國內外公認的重大挑戰。

幾十年來，為了提高航天嵌入式軟件的質量，軟件工作者開展了大量的工作，取得了很好的成效。然而，動態時序、控制行為和程序實現等深層次的軟件問題仍時有發生。

總體而言，現有的研制方法對人的能力、經驗依賴較大；針對軟件研制中的部分問題有一些解決辦法，但還沒有形成系統的解決方案，很難滿足航天任務變化快、進度緊、質量高的需求。因此，研究系統的嵌入式軟件可信性保障理論、方法、工具和環境已非常迫切。

由此推而廣之，中國裝備制造業尚未足夠強大，不少方面也“缺芯少魂”，這“魂”就是軟件。長期以來，國內大批設備依賴舶來引進，甚至包括地鐵等軌交基礎設施也是以進口為主，各有各的來路。隨著信息化、數字化、智能化，萬物運行從獨立封閉狀態發展到工業互聯網時代，如何確保關鍵領域的工控軟件不是一個個“黑盒子”，沒有后門也沒有漏洞？

在中國科學學院院士、華東師范大學軟件工程學院創院院長何積豐看來，這些都構成了國家整體安全的基本支撐面，要形成一個巨大的安全保障閉環，就像繡花功夫一樣急也急不來。有些情況下，軟件缺陷稍縱即逝，卻慢慢累積著，一個周期連到下一個周期，一個部件影響下一個部件，最終以故障形式出現。軟件人和軟件分析工具就要像過電影畫面一樣一幀幀看，讓“時間切片”一步步走，確保每條代碼萬無一失。

【攻克軟件可信保障技術三大難題】

十年磨一劍，磨刀石在哪？“控制軟件是工業重大裝備的中樞，是國家利器。要讓它足夠鋒利，就需要優良的磨刀石。”何積豐這位軟件界程序統一理論學派的開創者說，“我們就是把鑄劍的磨刀石做好做精，這樣來提高重大裝備核心控制軟件的質量，確保它們安全可信。”

解放日報·上觀新聞記者了解到，自2008年1月起，作為上海市科技進步特等獎項目第一完成人的何積豐院士，擔任國家自然科學基金委“可信軟件基礎研究”重大研究計劃首席科學家，支持全國科研院所涉及百業的相關課題達107項，迄今整整13年過去了。

作為上海市科技功臣和教育功臣，何積豐帶著整支團隊沖上一線。“我們的科學研究工作，是從產業實際出發，提煉科學問題；再通過研究成果的應用，來驗證我們的想法；最終形成核心技術，去解決國家所面臨的問題。”他說。而80后中，主持工作的軟件工程學院年輕院長陳銘松和團隊成員一起，深入行業企業打交道、“破黑盒”，以解決軟件可信保障技術的三大難題。

比如，軟件復雜性“分析難”：一份用戶需求文件可能好幾百頁，同時存在網絡延遲多變等運行環境的不確定性；又如，軟件正確性“驗證難”：以主流航空航天器百萬行級別的大規模代碼為例，必須讓代碼自動生成替代人工編寫代碼；再如，軟件可靠性“保障難”：接受國際測評標準嚴、投入大、周期長，軟件測試要占到開發成本一半左右。

“如果‘閉門造車’，可能‘水土不服’。”陳銘松介紹，卡斯柯信號有限公司就是此次項目團隊深入的行業企業之一，也是項目攻關的參研單位之一。2012年何積豐院士團隊與卡斯柯合作至今，其產品不僅已成功部署于上海軌道交通17號線，還服務于東非地區的第一條城市輕軌——埃塞俄比亞首都亞的斯亞貝巴輕軌，后者也成為中國第一套“走出去”的自主列車運行控制系統解決方案。

歷經十余年深入研究、實操實戰，他們一屆一屆接力，攻克了三大難題，也讓近千名高端軟件人才從這個大項目平臺出發，走向全國近百家企業，投身于軌道交通、航空航天、汽車電子和電力控制等諸多領域。

【像淘寶一樣上網獲得共性軟件服務】

值得一提的是，在上海市科技進步特等獎的獲獎證書上，除了第一完成單位華東師大外，其余6家都是中電科、普華等企業。可以說，一條產教學研協同創新的路徑，是這項“核高基”技術成功應用的必經之途。

卡斯柯研究設計院副院長周庭梁介紹，雙方依托院士專家工作站及上海軌道交通無人駕駛列控系統工程技術研究中心，針對卡斯柯自主研發的TRANAVI列車運行控制系統的核心控制軟件，進行了軟件形式化技術研究突破，產品滿足第三方國際評估機構SIL4安全認證要求。

來自申通地鐵集團技術中心的技術總監萬勇兵也透露，擁有700多公里里程、400余座車站的上海軌道交通，為對接國家自主可控戰略需求，聘請何積豐院士擔綱首席科學家，將高可信技術應用于“智慧地鐵”建設之中，助力上海保持在國內外城市軌交行業的技術領先地位和持續快速發展。

不論是針對空天、汽車還是電力的中樞神經，可控可信的共性技術即通用工具，用何積豐的話比方，就是讓不同行業的企業都能像淘寶一樣在網上獲得軟件服務。從體制機制層面上，在該項目支持下，作為支撐上海科創中心“四梁八柱”的重要創新力量——上海工業控制系統安全創新功能型平臺應運而生，成為上海市首批推動建設的18個研發與轉化功能型平臺之一。平臺骨干技術團隊成員，不少也是來自華東師大軟件工程學院的教授，現已形成系統化的自主可控軟件開發工具鏈，覆蓋了重大工業裝備核心控制軟件開發的全生命周期。

數據顯示，這項特等獎項目研究期間，共授權發明專利27項，獲得軟件著作權62項，制定行業標準2項，出版英文專著1本，發表高水平論文60篇……總體上，項目面向各行各業新增直接經濟效益和利潤累計超14.2億元，間接帶動了千億產值的產業效益。

項目團隊表示，未來將繼續為國產大飛機、深空探測和下一代城市軌交列車運行控制系統等重大國家級技術攻關提供共性技術，形成自主可控軟件人才和產業集聚效應，引領我國自主可控軟件產業發展，在國際上也形成高端裝備核心軟件的“中國造”品牌。他們說，“給國產裝備用，更要給國外設備用。”

分享讓更多人看到