從神舟天宮無人交會對接,到首條無人駕駛地鐵線,中樞神經可控可信...

天宮一號與神舟飛船自動對接，上海地鐵線首次實現無人駕駛，還有嫦娥三期地月間高速再入返回……這些無人奇蹟的背後，恰恰是人類將最大的智慧賦予最好的機器。

19日，由華東師範大學牽頭的《面向重大工業裝備核心控制軟體的安全可信保障技術及應用》項目摘得2019年度上海市科技進步特等獎。我國航空航天、軌道交通、電力控制等安全攸關領域，因此都有了中國人自主可控、高度可信的中樞神經。

僅空天領域，從神舟七號到風雲四號，項目技術就已在50餘個航天任務中成功應用。總體上，項目面向各行各業新增直接經濟效益和利潤累計超14.2億元，間接帶動了千億產值的產業效益。

【一位將帥，出思想方法】

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

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

自2008年1月起，作為此項目第一完成人的何積豐院士，擔任國家自然科學基金委「可信軟體基礎研究」重大研究計劃首席科學家，支持全國科研院所涉及百業的相關課題達107項。整整12年過去了，何積豐也77歲了。

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

作為上海市科技功臣、上海市教育功臣以及全國優秀共產黨員，何積豐帶著整支團隊衝上一線。項目研究期間，共授權發明專利27項，獲得軟體著作權62項，制定行業標準2項，出版英文專著1本，發表高水平論文60篇……「我們的科學研究工作，是從產業實際出發，提煉科學問題；再通過研究成果的應用，來驗證我們的想法；最終形成核心技術，去解決國家所面臨的問題。」他說。

【一隊人馬，解三大難題】

將帥麾下，才俊雲集。特等獎項目組成員來自五湖四海，既有從美國、日本回來的海歸，也有國內兄弟院校培養的博士。華東師大軟體工程學院黨委書記錢海峰表示，隊伍裡80後也已經挑大梁，在整個項目15名主要完成人中，80後青年科研工作者就有6名。

作為主持工作的軟體工程學院年輕院長，陳銘松從事可信計算研究已多年，經國內導師推薦，歸國後即慕名加入何積豐團隊。他告訴記者，高端軟體領域美方企業的關鍵核心崗位通常很難接受中國學子，「當真正觸及核心技術，或多或少受到限制。」在國內，陳銘松和團隊成員一起，深入行業企業打交道、「破黑盒」，以解決軟體可信保障技術的三大難題。

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

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

「何老師常常強調，一切都從實際出發，到行業一線找需求。」80後的院長助理繆煒愷博士說，項目團隊一直傳遞這樣的文化，不只是關心發文章或拿工分。歷經十餘年深入研究、實操實戰，他們一屆一屆接力，攻克了三大難題，也讓近千名高端軟體人才從這個大項目平臺出發，走向全國近百家企業，投身於軌道交通、航空航天、汽車電子和電力控制等諸多領域。

【一群同行，創十數億效益】

「為啥你的軟體可靠，為啥不用國外的」「不是禁運，就是特貴，有錢也沒用」……不論是中國電子科技集團公司第三十二所總工張激，還是普華基礎軟體股份有限公司總經理江水，與高校合作攻關汽車電子軟體打入歐美市場的他們，最初在業內碰上的幾乎都是類似問題。

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

從院士專家工作站落戶國內同行排名第一的卡斯柯信號有限公司，到中電科32所與華東師大組建國家工程中心，在這些企業科研人員口中，「聯合實驗室」可謂關鍵詞。

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

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

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

解放日報·上觀新聞記者了解到，目前已掌握自己手中的完全智慧財產權的形式化建模、測試與驗證工具達11款，已形成商業化產品的有6款。其中，軟體自動化測試工具SmartUnit更是成為國內首款通過國際上公認標準TUV功能安全認證的測試工具。近3年來，工具鏈產品銷售額即達1.5億元。

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