摘要
简要介绍全舰计算环境(Total Ship Computing Environment,TSCE)的基本概念、相关组成、体系架构、安全需求分析以及美军TSCE设计经验对我军舰艇发展的启示。针对TSCE的安全性未知问题,我们引入了形式化验证方法。首先,使用全自动的模型检测方法验证TSCE子集;然后,使用形式推理的方式半自动半人工的验证TSCE全集。复杂度分析揭示了新方法的效率。最后,得出结论,本文提出的TSCE形式化验证方案可望与传统的软件工程方法优势互补,协同验证TSCE是否满足包括安全性在内的相关性质需求。
It briefly introduced the basic concepts, related components, architecture, security requirements analysis and the experience of US military TSCE design experience in the development of our military ships in the Total Ship Computing Environment.Aiming at the technical safety unknown of TSCE.we have introduced a formal verification method.First, a model checking method can verify a subset ofa TSCE automatically. Second, the formal deduce method can verify a TSCE semi-automatically. The complexity analysis shows that the new methods are efficient.Finally, it is concluded that the TSCE formal verification scheme proposed in this paper is expected to be complementary to the traditional software engineering methods to verify whether TSCE meets the related nature requirements including security.
出处
《数字技术与应用》
2017年第6期140-141,143,共3页
Digital Technology & Application
关键词
全舰计算环境
形式化验证
模型检测
形式推理
total ship computing environment
formal verification
model checking
formal deduce
