全艦計算環境形式化驗證算法

朱維軍+樊永文+聶凱

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

關鍵詞：全艦計算環境；形式化驗證；模型檢測；形式推理

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

1 引言

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

全艦計算環境是一種革新性的概念，它以網絡為中心，集成了作戰系統、預警系統、動力系統、武器系統與指揮控制系統，整合上述系統所需設備在TSCE上統一規劃、集中管理、動態共用，以為全艦提供基礎計算服務支持，從而形成統一的網絡中心戰單元，促進跨平臺、跨領域協同作戰，提升作戰效率。據報道，TSCE的部署有助于所在艦艇應對處理海基彈道導彈的威脅[3]。

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

2 相關工作

2.1 全艦計算環境（TSCE）

TSCE 由上層的作戰應用軟件包和下層的“全艦計算環境基礎設施”（Total Ship Computing Environment infrastructure，TSCEi）兩部分組成[4]。以開放式體系結構（OA）為基礎，基于全艦計算環境基礎設施所提供的平臺化計算支持。TSCE 體系結構是標準的五級開放式體系結構。下面分別簡介這些系統模塊。

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

2.1.1 OA

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

開放體系結構計算環境（OACE）中資源具有可重用性、共享性、異構性、廣域性等特點。它有七層結構：應用層、協議層、核心服務層、中間件層、基礎服務層、操作系統層、資源層。

2.1.2 TSCEi

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

TSCEi的結構分為硬件層、操作系統層、中間件層以及基礎結構服務層。

2.1.3 TSCE體系結構

TSCE體系結構是標準的五級開放式體系結構[7]，由硬件層、操作系統層、中間件層和通用服務接口層組成。艦艇各類應用通過應用軟件部署和標準服務接口，使用TSCE的硬件和服務軟件，完成各自的計算/作戰任務。

2.2 TSCE的安全需求

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

2.3 美軍TSCE設計分析

當今軟件密集型復雜武器系統的典型代表—TSCE，它的研制模式已經由原來的基于文檔轉變為現在的基于模型的系統工程[8]。系統集成由一些豐富的形式化模型來定義。DDG—1000的TSCE是一項相當復雜的系統工程。以軟件開發為主，目前代碼規模已達到1700萬行。

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

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

3 TSCE的模型檢測算法

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

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

定理1：算法1的復雜度為指數級。

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

命題得證。

圖2初步示意了算法1的模擬運行時間。從該圖可見，在運行規模可接受的范圍內算法1的效率是可行的。

4 TSCE的形式化推理

可見，這是一種從抽象到實現的逐步求精的面向系統開發與驗證的形式化方法。

5 結語

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

6 致謝

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

參考文獻

[1]秦藝丹.全艦計算環境（TSCE）技術的發展現狀[EB/OL].科普中國，[2015-10-30].

[2]張偉.美國海軍全艦計算環境發展及關鍵技術[J].船舶科學技術，2016，38，（7）： 148-152.

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

[4]金剛.全艦計算環境安全體系結構研究[J].船舶電子工程，2016，36，（11）：5-7，62.

[5]葛麗.基于博弈的開放體系結構任務調度研究[D].哈爾濱：哈爾濱工程大學.2012.

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

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

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

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

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

[11]劉杰生.美軍全艦計算環境質量屬性簡析及啟示[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