全艦計算環(huán)境形式化驗證算法

朱維軍+樊永文+聶凱

摘要：簡要介紹全艦計算環(huán)境（Total Ship Computing Environment，TSCE）的基本概念、相關(guān)組成、體系架構(gòu)、安全需求分析以及美軍TSCE設(shè)計經(jīng)驗對我軍艦艇發(fā)展的啟示。針對TSCE的安全性未知問題，我們引入了形式化驗證方法。首先，使用全自動的模型檢測方法驗證TSCE子集；然后，使用形式推理的方式半自動半人工的驗證TSCE全集。復雜度分析揭示了新方法的效率。最后，得出結(jié)論，本文提出的TSCE形式化驗證方案可望與傳統(tǒng)的軟件工程方法優(yōu)勢互補，協(xié)同驗證TSCE是否滿足包括安全性在內(nèi)的相關(guān)性質(zhì)需求。

關(guān)鍵詞：全艦計算環(huán)境；形式化驗證；模型檢測；形式推理

中圖分類號：TP301.6 文獻標識碼：A 文章編號：1007-9416（2017）06-0140-02

1 引言

未來海戰(zhàn)的模式將由“平臺中心戰(zhàn)”轉(zhuǎn)向“網(wǎng)絡(luò)中心戰(zhàn)”[1]。網(wǎng)絡(luò)中心化逐步成為美國海軍編隊電子信息系統(tǒng)和艦船電子信息系統(tǒng)的發(fā)展方向[2]。在此背景下，“朱姆沃爾特”級驅(qū)逐艦DDG-1000成為第一艘全面實施全艦計算環(huán)境（TSCE）的美國新一代軍艦，該艦于2012年交付使用，2014年形成初步作戰(zhàn)能力[2]。

全艦計算環(huán)境是一種革新性的概念，它以網(wǎng)絡(luò)為中心，集成了作戰(zhàn)系統(tǒng)、預警系統(tǒng)、動力系統(tǒng)、武器系統(tǒng)與指揮控制系統(tǒng)，整合上述系統(tǒng)所需設(shè)備在TSCE上統(tǒng)一規(guī)劃、集中管理、動態(tài)共用，以為全艦提供基礎(chǔ)計算服務(wù)支持，從而形成統(tǒng)一的網(wǎng)絡(luò)中心戰(zhàn)單元，促進跨平臺、跨領(lǐng)域協(xié)同作戰(zhàn)，提升作戰(zhàn)效率。據(jù)報道，TSCE的部署有助于所在艦艇應(yīng)對處理?；鶑椀缹椀耐{[3]。

作為美國海軍新一代艦載系統(tǒng)集成技術(shù)，TSCE是邁向“網(wǎng)絡(luò)中心戰(zhàn)”的一個重要里程碑[2]。美軍已表示其下一代艦艇的開發(fā)和現(xiàn)有艦艇的升級都將采用TSCE[1][2][3]。然而，TSCE技術(shù)本身是否可完全滿足實戰(zhàn)需求？該技術(shù)是否安全、有效、可靠？從已有的公開出版文獻看，目前未見報道。這是本文擬研究的問題。

2 相關(guān)工作

2.1 全艦計算環(huán)境（TSCE）

TSCE 由上層的作戰(zhàn)應(yīng)用軟件包和下層的“全艦計算環(huán)境基礎(chǔ)設(shè)施”（Total Ship Computing Environment infrastructure，TSCEi）兩部分組成[4]。以開放式體系結(jié)構(gòu)（OA）為基礎(chǔ)，基于全艦計算環(huán)境基礎(chǔ)設(shè)施所提供的平臺化計算支持。TSCE 體系結(jié)構(gòu)是標準的五級開放式體系結(jié)構(gòu)。下面分別簡介這些系統(tǒng)模塊。

下面給出具體的算法描述：

2.1.1 OA

OA[5]是當前海軍作戰(zhàn)領(lǐng)域研究的一種先進的技術(shù)，它作為一個綜合的策略，目標是將允許使用和實現(xiàn)海軍領(lǐng)域中覆蓋海、陸、空和水下平臺的軟件構(gòu)件、測試案例和場景、模型、仿真、設(shè)計和體系結(jié)構(gòu)、以及人機接口等資源的共享。

開放體系結(jié)構(gòu)計算環(huán)境（OACE）中資源具有可重用性、共享性、異構(gòu)性、廣域性等特點。它有七層結(jié)構(gòu)：應(yīng)用層、協(xié)議層、核心服務(wù)層、中間件層、基礎(chǔ)服務(wù)層、操作系統(tǒng)層、資源層。

2.1.2 TSCEi

作為TSCE的主要技術(shù)和主要組成—全艦計算環(huán)境基礎(chǔ)設(shè)施TSCEi包括了網(wǎng)絡(luò)設(shè)備、計算設(shè)備、存儲設(shè)備、顯示設(shè)備和操控設(shè)備等硬件設(shè)備，以及一組核心、通用的基礎(chǔ)軟件。全艦所有應(yīng)用軟件都運行于其之上，為運行于其頂層的應(yīng)用程序提供統(tǒng)一的信息交換、信息處理、信息存儲、信息分發(fā)、信息安全和保密等服務(wù)，實現(xiàn)艦艇上所有系統(tǒng)的綜合信息管理，提供信息的實時處理與分發(fā)、數(shù)據(jù)庫存儲與訪問等服務(wù)實現(xiàn)了艦船上所有艦載系統(tǒng)的無縫集成。文獻[6]分析TSCEi 的結(jié)構(gòu)和組成，得出結(jié)論認為公共計算服務(wù)環(huán)境是未來艦船提高綜合作戰(zhàn)能力和信息化水平的有效手段。

TSCEi的結(jié)構(gòu)分為硬件層、操作系統(tǒng)層、中間件層以及基礎(chǔ)結(jié)構(gòu)服務(wù)層。

2.1.3 TSCE體系結(jié)構(gòu)

TSCE體系結(jié)構(gòu)是標準的五級開放式體系結(jié)構(gòu)[7]，由硬件層、操作系統(tǒng)層、中間件層和通用服務(wù)接口層組成。艦艇各類應(yīng)用通過應(yīng)用軟件部署和標準服務(wù)接口，使用TSCE的硬件和服務(wù)軟件，完成各自的計算/作戰(zhàn)任務(wù)。

2.2 TSCE的安全需求

全艦計算環(huán)境下的應(yīng)用帶來了安全需求的變化。例如在應(yīng)用安全上有：身份認證、授權(quán)訪問、數(shù)據(jù)存儲保護等。在TSCE進行基礎(chǔ)資源統(tǒng)一分配時出現(xiàn)了：認證、授權(quán)、機密性、完整性、不可抵賴性等基本安全需求。如何滿足這些基本安全需求，將對艦只作戰(zhàn)產(chǎn)生一定影響。

2.3 美軍TSCE設(shè)計分析

當今軟件密集型復雜武器系統(tǒng)的典型代表—TSCE，它的研制模式已經(jīng)由原來的基于文檔轉(zhuǎn)變?yōu)楝F(xiàn)在的基于模型的系統(tǒng)工程[8]。系統(tǒng)集成由一些豐富的形式化模型來定義。DDG—1000的TSCE是一項相當復雜的系統(tǒng)工程。以軟件開發(fā)為主，目前代碼規(guī)模已達到1700萬行。

2.4 TSCE對我軍艦艇信息化的啟示

文獻[9]初步提出一種建議，關(guān)于我軍全艦計算環(huán)境的體系架構(gòu)及全艦信息化總體概念方案，給出我軍全艦計算環(huán)境及信息化集成的發(fā)展建議，為我軍全艦信息系統(tǒng)的發(fā)展提供參考[9]。他山之石，可以攻玉，關(guān)于外軍TSCE對我軍艦艇信息化建設(shè)的啟示，這方面已有相當數(shù)量的文獻公開刊登在學術(shù)期刊，篇幅所限，本文不再詳述。

3 TSCE的模型檢測算法

就通用計算而言，以測試為基礎(chǔ)的傳統(tǒng)軟件工程方法無法杜絕軟件錯誤。已有報道表明，軟件運行出錯導致了諸如火箭發(fā)射失敗等災(zāi)難性后果[10]。為此，研究人員已開發(fā)出若干形式化方法以驗證通用關(guān)鍵計算系統(tǒng)的一系列重要性質(zhì)。就TSCE專用應(yīng)用領(lǐng)域而言，使用形式化驗證方法與工具也可望發(fā)現(xiàn)系統(tǒng)錯誤。目前為止，在該專用領(lǐng)域常用的語言與工具主要包括：UML、XML，以及一些軍用專用語言工具[8]。然而，這些工具僅僅基于半形式化的方法，它們形式化程度不足。從公開報道的文獻來看，現(xiàn)有的對TSCE質(zhì)量評估的方式僅依靠包括軟件測試在內(nèi)的非形式化的傳統(tǒng)軟件工程方法[2][11]。endprint

MVSL是一種功能強大的形式化語言與工具[12]。在本文設(shè)計的方案中，我們使用該工具對TSCE實施形式化驗證，其中模型檢測用于全自動驗證TSCE部分系統(tǒng)的性質(zhì)，而形式推理（如第4節(jié)所示）則用于半自動半人工的驗TSCE系統(tǒng)的性質(zhì)。

定理1：算法1的復雜度為指數(shù)級。

證明：算法1由一個循環(huán)組成。循環(huán)體只有一條語句。它調(diào)用MVSL模型檢測算法，該算法的時間復雜度為非初等（一階至高階指數(shù)）[12]，該循環(huán)體被執(zhí)行k次，因此整個循環(huán)需要指數(shù)級時間才能完成，故此，算法1需要時間為指數(shù)級。

命題得證。

圖2初步示意了算法1的模擬運行時間。從該圖可見，在運行規(guī)?？山邮艿姆秶鷥?nèi)算法1的效率是可行的。

4 TSCE的形式化推理

可見，這是一種從抽象到實現(xiàn)的逐步求精的面向系統(tǒng)開發(fā)與驗證的形式化方法。

5 結(jié)語

本文初步給出一種 TSCE 形式化驗證方案，瞄準輔助提升 TSCE 的信息裝備質(zhì)量。特別是，文獻[4]與文獻[9]指出 TSCE 技術(shù)面臨的安全需求、實時需求與交互需求。新的基于形式化的方法可望與傳統(tǒng)的軟件工程方法協(xié)同，共同驗證 TSCE 是否滿足上述需求，從而有助于更好的適應(yīng)以網(wǎng)絡(luò)中心戰(zhàn)為核心的未來海戰(zhàn)戰(zhàn)場的需求。這是新方法的潛在應(yīng)用前景。

6 致謝

感謝文后參考文獻的作者，本文作者正是在閱讀這些公開出版文獻的基礎(chǔ)上，給出我們的個人思考與個人觀點。

參考文獻

[1]秦藝丹.全艦計算環(huán)境（TSCE）技術(shù)的發(fā)展現(xiàn)狀[EB/OL].科普中國，[2015-10-30].

[2]張偉.美國海軍全艦計算環(huán)境發(fā)展及關(guān)鍵技術(shù)[J].船舶科學技術(shù)，2016，38，（7）： 148-152.

[3]郭隆華. "朱姆沃爾特"級驅(qū)逐艦全艦計算環(huán)境研究取得進展[J].船舶科學技術(shù)，2008，（5）：164-164.

[4]金剛.全艦計算環(huán)境安全體系結(jié)構(gòu)研究[J].船舶電子工程，2016，36，（11）：5-7，62.

[5]葛麗.基于博弈的開放體系結(jié)構(gòu)任務(wù)調(diào)度研究[D].哈爾濱：哈爾濱工程大學.2012.

[6]董曉明，石朝明，黃坤，等.美海軍 DDG-1000 全艦計算環(huán)境體系結(jié)構(gòu)探析[J].中國船舶研究，2012，7，（6）：7-14.

[7]裴曉黎.美海軍TSCE 設(shè)計剖析及對我軍信息系統(tǒng)集成模式的示[J].計算機與數(shù)字工程，2015，（9）：1607-1614.

[8]董曉明，胡洋.基于模型系統(tǒng)工程在全艦計算環(huán)境集成框架的應(yīng)用概覽[J].中國船舶研究，2016， 11（6）：124-135.

[9]徐勇.全艦計算環(huán)境及信息化總體概念方案研究[J].船舶電子工程，2016，36（11）：12-19，88.

[10]楊啟亮，邢建春，王平. 安全關(guān)鍵系統(tǒng)及其軟件方法[J].計算機應(yīng)用與軟件，2011，28（2）：129-138，147.

[11]劉杰生.美軍全艦計算環(huán)境質(zhì)量屬性簡析及啟示[J].船舶電子工程，2016，36（7）：10-13.

[12]YU Y， DUAN Z H， TIAN C. Model Checking C Programs with MSVL [M].SOFL [C]，2012：87-103.endprint