军用指挥控制软件可信性分析与验证技术

摘要

With improving the informatization level of weapon equipment,the reliability of military command and control software is directly related to its overall effectiveness. On basis of the research of traditional software quality assurance technologies,the formal method based software analysis and verification technology are presented according to the characteristic of the military command and control software. It includes:the formal safety specification technology,the verification technology of the command software based on model checking and the analysis technology of the control software based on static analysis. In the end,the formal analysis and verification integrated environment suitable for the life cycle development of the command and control software are put forward.%随着武器装备信息化程度越来越高,军用指挥控制软件的可信性直接关系到装备整体效能的发挥.在对传统软件质量保证技术研究的基础上,结合军用指挥控制软件的特点,提出了基于形式化方法的软件分析与验证技术.分别从安全性质形式化规约技术、基于模型检验的指挥软件验证技术和基于静态分析的控制软件分析技术三方面保证军用指挥控制软件的可信性,最后,提出了适用于指挥控制软件全生命周期开发的形式化分析与验证集成环境.