CAJ | 학술논문

随着武器装备信息化程度越来越高,军用指挥控制软件的可信性直接关系到装备整体效能的发挥.在对传统软件质量保证技术研究的基础上,结合军用指挥控制软件的特点,提出了基于形式化方法的软件分析与验证技术.分别从安全性质形式化规约技术、基于模型检验的指挥软件验证技术和基于静态分析的控制软件分析技术三方面保证军用指挥控制软件的可信性,最后,提出了适用于指挥控制软件全生命周期开发的形式化分析与验证集成环境.
수착무기장비신식화정도월래월고,군용지휘공제연건적가신성직접관계도장비정체효능적발휘.재대전통연건질량보증기술연구적기출상,결합군용지휘공제연건적특점,제출료기우형식화방법적연건분석여험증기술.분별종안전성질형식화규약기술、기우모형검험적지휘연건험증기술화기우정태분석적공제연건분석기술삼방면보증군용지휘공제연건적가신성,최후,제출료괄용우지휘공제연건전생명주기개발적형식화분석여험증집성배경.
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.