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

Static Analysis and Verification Technology for Reliability of Military Command and Control Software

作　　者：许婧祺[1] 董龙明 郝丽波[1] 

机构地区：[1]湖南机电职业技术学院,长沙410073 [2]总装备部驻南京地区军事代表室,南京210000

出　　处：《火力与指挥控制》2015年第8期176-180,共5页Fire Control & Command Control

基　　金：湖南省科技厅应用基础研究项目(2014FJ3050);湖南省教育科学规划基金资助项目(XJK013CXX003)

摘　　要：随着武器装备信息化程度越来越高,军用指挥控制软件的可信性直接关系到装备整体效能的发挥。在对传统软件质量保证技术研究的基础上,结合军用指挥控制软件的特点,提出了基于形式化方法的软件分析与验证技术。分别从安全性质形式化规约技术、基于模型检验的指挥软件验证技术和基于静态分析的控制软件分析技术三方面保证军用指挥控制软件的可信性,最后,提出了适用于指挥控制软件全生命周期开发的形式化分析与验证集成环境。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.

关 键 词：军用指挥控制软件 分析与验证技术 模型检验 静态分析 

分 类 号：TP39[自动化与计算机技术—计算机应用技术]