全舰计算环境形式化验证算法

朱维军+樊永文+聂凯

摘要：简要介绍全舰计算环境（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