摘要
随着武器装备信息化程度越来越高,军用指挥控制软件的可信性直接关系到装备整体效能的发挥。在对传统软件质量保证技术研究的基础上,结合军用指挥控制软件的特点,提出了基于形式化方法的软件分析与验证技术。分别从安全性质形式化规约技术、基于模型检验的指挥软件验证技术和基于静态分析的控制软件分析技术三方面保证军用指挥控制软件的可信性,最后,提出了适用于指挥控制软件全生命周期开发的形式化分析与验证集成环境。
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.
出处
《火力与指挥控制》
CSCD
北大核心
2015年第8期176-180,共5页
Fire Control & Command Control
基金
湖南省科技厅应用基础研究项目(2014FJ3050)
湖南省教育科学规划基金资助项目(XJK013CXX003)
关键词
军用指挥控制软件
分析与验证技术
模型检验
静态分析
military command and control software
analysis and verification technology
model checking
static analysis
