朱维军+樊永文+聂凯

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