基于时序逻辑的仿真系统行为验证方法  

Method of simulation system behavior validation based on temporal logic

作　　者：彭丹华 吴正雄 李廷鹏 耿宏峰[1] PENG Danhua;WU Zhengxiong;LI Tingpeng;GENG Hongfeng(Unit 63892 of PLA,Luoyang 471003,China;State Key Laboratory of Complex Electromagnetic Environment Effects on Electronics and Information System,Luoyang 471003,China)

机构地区：[1]中国人民解放军63892部队,河南洛阳471003 [2]电子信息系统复杂电磁环境效应国家重点实验室,河南洛阳471003

出　　处：《现代电子技术》2023年第5期175-179,共5页Modern Electronics Technique

摘　　要：仿真系统行为可信性评估是一项复杂的任务,需要综合利用多种方法、从多个角度对仿真系统的行为进行验证。针对仿真系统行为验证既需要具有客观性又需要考虑领域专家宝贵经验的需求,借鉴形式化验证技术的思想,提出基于时序逻辑的仿真系统行为验证方法。该方法首先根据真实系统和实测数据,结合专家经验,对所关注的仿真系统行为属性进行提取;其次,利用时序逻辑语言对提取的待验证属性进行形式化描述;然后,运行仿真系统并获得相应的输出数据,利用验证算法自动检验仿真数据是否满足给定的属性,从而实现行为验证;基于对武器装备体系对抗仿真领域的验证属性分析,选取度量区间时序逻辑作为属性的形式化描述语言;最后,通过一个防空对抗仿真系统的验证示例,表明了该方法的有效性。The credibility evaluation of simulation systems is a complex task which requires the comprehensive use of multiple methods to synthetically validate the systems′ behavior from different aspects. In allusion to the requirements that the behavior validation of simulation systems should be objective and consider the valuable experience of domain experts,a method of the simulation system behavior verification based on temporal logic is proposed by means of formal validation technology. According to the real system,measured data and expert experience,the behavior properties of the simulation system are extracted. The temporal logic languages are used to conduct the formalization description of the extracted property under validation. And then corresponding output data is collected by the operation of the simulation system,and the checking algorithm is used to automatically check whether the simulation data satisfy the given properties. On the basis of the analysis of validation properties of weapon equipment simulation systems,the metric interval temporal logic is selected as the formalization description language of the properties. An example of an air defense simulation system is utilized to show the effectiveness of this method.

关 键 词：仿真系统 行为验证 可信性评估 时序逻辑 行为属性提取 形式化描述 数据检验 

分 类 号：TN919-34[电子电信—通信与信息系统]