向时间自动机转换的军事电子信息系统性质验证  

Verification of Military Electronic Information Systems Based on Timed Petri Nets Transforming to Timed Automata

作　　者：邓小妮[1] 罗雪山[2] 

机构地区：[1]国防科技大学人文与社会科学学院,长沙410073 [2]国防科技大学信息系统与管理学院,长沙410073

出　　处：《火力与指挥控制》2011年第12期134-137,共4页Fire Control & Command Control

基　　金：武器装备基金资助项目(51406010704KG0143)

摘　　要：日益复杂的军事电子信息系统面临正确性验证挑战,形式化验证方法如模型检验技术成为必需。给出基于时间Petri网表示的军事电子系统模型PMES的定义,然后给出PMES模型转换为时间自动机网的步骤,利用已有的基于时间自动机的模型检验工具对系统性质进行验证;系统的性质要求用时序逻辑语言CTL或TCTL公式表示。雷达干扰机系统说明了该方法的实际应用效果。The ever increasing complexity of military electronic information systems poses a challenge in verifying their correctness.Formal verification methods such as model checking that overcome the limitation of traditional techniques are needed.In this paper,the semantics of PMES,a Petri net based model aimed to represent military electronic systems,are formally defined.A procedure to translate PMES into timed automata is introduced in order to use existing verification tools to check properties expressed as CTL and TCTL formulas.The Radar jammer system is studied to illustrate the applicability of the approach to practical systems.

关 键 词：形式化验证 模型检验 PETRI网 时间自动机 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]