“高可信”是什么？

　　用王戟的話說，軟件信息系統(tǒng)會“生病”，高可信軟件就是給軟件“看病”的工具，用來檢查軟件的性能是否符合人們的預(yù)期?！跋喈?dāng)于給軟件做一個CT掃描，看看哪些地方可能有問題，盡早解決?！?/p>

　　王戟又是誰？

　　他是國防科技大學(xué)計算機學(xué)院研究員，是不滿14歲考上大學(xué)的少年英才，是43歲高位截肢后仍坐著輪椅沖鋒在科研一線的領(lǐng)軍人才，是用一篇論文開創(chuàng)了中國高可信軟件技術(shù)研究領(lǐng)域的開拓者。

　　當(dāng)王戟的名字與“高可信”這個名詞同時出現(xiàn)，意味著什么？

　　在中國科學(xué)院院士、國防科大教授王懷民看來，在中國，一提到高可信軟件技術(shù)，就一定會想到王戟。尤其是在軍事領(lǐng)域，王戟的名字與“高可信”同時出現(xiàn)，“大家會有一種安全感，會想到為這種安全感作出重要貢獻的一位學(xué)者”。

　　從開辟一個新的研究領(lǐng)域，到取得一系列創(chuàng)新成果，再到成為一條人生道路，這便是王戟與高可信的故事。

　　要“可信”，還要“高”可信

　　2003年，一篇題為《高可信軟件工程技術(shù)》的論文發(fā)表在當(dāng)年第12期《電子學(xué)報》(增刊)上，作者是陳火旺、王戟、董威。這篇論文可以被視為中國計算機高可信軟件技術(shù)初始階段最重要的文章，為中國的計算機研究開辟了一個新的領(lǐng)域。提出“高可信軟件技術(shù)”這個前瞻性概念的人，正是王戟。

　　在此之前，國際上已有相關(guān)研究。隨著科學(xué)技術(shù)的發(fā)展，軟件的規(guī)模越來越龐雜，早已擺脫附屬于硬件的狀態(tài)。時至今日，在社會各行各業(yè)所使用的系統(tǒng)中，絕大部分的功能由軟件完成。也正因此，軟件的可靠性、安全性若不能得到保證，所造成的損失可能是災(zāi)難性的。無論是阿麗亞娜5型火箭升空后爆炸，還是英特爾公司召回有問題的芯片，歷史已有前車之鑒。

　　早在1992年，王戟在讀過一位外國專家的相關(guān)論文后，就開始思考軟件可靠性的問題，在日常工作中重點留意這個方向的內(nèi)容。博士生畢業(yè)前后，他做出的模型完成了對某些小型軟件的檢驗，取得了一定成果。1999年，王戟與老師、同事們赴北京參與航天測試任務(wù)的可靠性評估工作，拿出了新設(shè)計的一套度量工具。這是王戟在高可信軟件技術(shù)科研道路上的一次小試牛刀。

　　對于這一類研究，人們最早稱之為軟件的“可靠性研究”。但王戟認為，軟件研究的內(nèi)涵和外延都已發(fā)生變化，需要一個新的概念來概括。光叫“可靠”還不夠，“可信”更為恰當(dāng)，還要“高”可信。

　　“高可信這個詞實際上有一部分的內(nèi)涵繼承了以前的技術(shù)邏輯，但是在新的場景和需求下，它有更豐富的內(nèi)涵和外延，來牽引我們的技術(shù)進步。”王戟說。

　　為了達成軟件更高的可信度，王戟與他的團隊也要站得更高，瞄準(zhǔn)領(lǐng)域發(fā)展的前沿。因為高可信軟件的應(yīng)用場景更多體現(xiàn)在“關(guān)鍵軟件”中，關(guān)乎國家和軍隊建設(shè)的重點領(lǐng)域，是國家、軍隊對軟件需求中最重要的一個方面。這也注定了高可信軟件技術(shù)研究的學(xué)術(shù)前沿堆滿了難啃的“硬骨頭”。

　　十年磨一劍，科研要“立地”

　　最早，人們談到的軟件正確性、可靠性問題都具有明確的系統(tǒng)邊界，是在一個相對封閉的環(huán)境下、一個簡單的系統(tǒng)中找問題。王戟與老師、同事們深耕的高可信軟件技術(shù)則是處在一個開放、復(fù)雜的環(huán)境中，既要在“通用”的理論基礎(chǔ)上取得突破，又要進一步適配“專用”的應(yīng)用場景，面臨“通專結(jié)合”的挑戰(zhàn)。

　　這是中國高可信軟件技術(shù)研究發(fā)展的一個特點，也是一個難點。

　　其實，證明一款軟件可信程度的方法有很多，包括軟件驗證、工程化手段等。王戟團隊之所以深耕當(dāng)前領(lǐng)域，是因為高可信軟件技術(shù)具備嚴(yán)格的數(shù)學(xué)基礎(chǔ)?；A(chǔ)理論上的突破能夠保障算法的可靠性，提升高可信本身的可信度，使其保障能力更強。

　　王戟在校讀書時，中國的高可信軟件技術(shù)研究還在跟跑，到后來逐漸發(fā)展為并跑?！艾F(xiàn)在，我們在部分技術(shù)環(huán)節(jié)上，實際上已經(jīng)領(lǐng)跑了?！边@與國家整體的科技實力增長是一致的。比如，在航天這個高可信軟件的重要應(yīng)用方向上，中國的航天科技發(fā)展已經(jīng)處于國際領(lǐng)先水平，其所面臨的軟件可信度問題在國際上也是前沿問題。

　　另一方面，“高可信軟件不是一個停留在理論上的問題，它有很強的工程背景”。王戟說。

　　2015年，王戟擔(dān)任某國防973項目的技術(shù)首席專家，研究內(nèi)容就是高可信軟件技術(shù)。2021年，該項目通過驗收，順利結(jié)項。2025年，該項科研成果榮獲軍事科學(xué)技術(shù)進步獎一等獎。如今，這項成果十年磨一劍，已經(jīng)被應(yīng)用在航空航天、重大武器裝備等國之重器上。

　　在國防科技大學(xué)的師生中流傳著一句話：搞科研要“頂天立地”?！绊斕臁笔侵妇o跟研究領(lǐng)域內(nèi)學(xué)術(shù)發(fā)展的最新前沿動態(tài)；“立地”則是指注重成果轉(zhuǎn)化，讓科技成果真正落地生根、發(fā)揮實效。

　　目前，高可信軟件技術(shù)已經(jīng)在國家和軍隊建設(shè)的關(guān)鍵領(lǐng)域發(fā)揮了重要作用。但在王戟看來，高可信仍處在“立地”的過程中。國家、軍隊建設(shè)對高可信軟件的需求在不斷增長，這就需要高可信軟件技術(shù)也要不斷進步，去滿足增長的客觀需求。

　　我和高可信“永遠在路上”

　　經(jīng)過多年的發(fā)展，高可信軟件有了更加準(zhǔn)確的含義：它是通過程序分析和驗證技術(shù)確保極高的可靠安全性與保密安全性的軟件，其核心特征是通過形式化方法替代傳統(tǒng)測試手段，為國家安全、軍用裝備等相關(guān)領(lǐng)域提供嚴(yán)格保障。

　　王懷民認為，高可信軟件的重要性不只體現(xiàn)在給軟件“治病”，更體現(xiàn)在為軟件做“體檢”，體現(xiàn)在“治未病”上?！巴蹶捌鋱F隊就是在不斷探究‘體檢’的工具，讓我們能發(fā)現(xiàn)更多可能的‘病灶’，排查那些尚未對軟件的‘健康’產(chǎn)生致命性影響的隱患?！?/p>

　　如今，在大數(shù)據(jù)、云計算、人工智能飛速發(fā)展的時代，高可信軟件技術(shù)的內(nèi)涵與外延變得更加豐富，其發(fā)展同時面臨機遇與挑戰(zhàn)。

　　“人工智能是目前技術(shù)發(fā)展一個非常重要的方向，毫無疑問是一個熱點，給我們帶來了更強大的推動力，在各行各業(yè)都是個倍增器?！蓖蹶硎?，人工智能也帶來了一些困擾和挑戰(zhàn)，特別是在其可信評價方面。這也是王戟與團隊研究的一個方面，即如何用高可信軟件對人工智能系統(tǒng)作出評價，讓AI技術(shù)更加安全可信。

　　當(dāng)前，王戟與其團隊正圍繞人工智能大模型的研發(fā)與性能評測開展某項重大工程研究攻關(guān)，努力在前沿性、戰(zhàn)略性領(lǐng)域贏得主動。

　　王戟坦言：“我希望看到我們的技術(shù)用在一批國之重器上，用在國家的關(guān)鍵領(lǐng)域中，能夠保障戰(zhàn)斗力的生成。我也希望我們的技術(shù)能夠往前發(fā)展，來引領(lǐng)新質(zhì)戰(zhàn)斗力的生成?！?/p>

　　高可信軟件技術(shù)還有多遠的路要走？對于這個問題，王戟的回答是“永遠在路上”。只要信息技術(shù)、智能技術(shù)不斷前進，軟件作為這些技術(shù)的基本載體就會不停地發(fā)展、變化。相應(yīng)地，軟件的保障技術(shù)也要不斷發(fā)展，高可信軟件技術(shù)“會一直走在這條路上”。

　　“您會一直走在這條道路上嗎？”中新社記者問到。

　　“我會一直在。”王戟說。

　　作者：李純 曾鈺婷

　　來源：中新社微信公眾號