火力与指挥控制2011，Vol.36Issue(12)：134-137,4.
向时间自动机转换的军事电子信息系统性质验证
Verification of Military Electronic Information Systems Based on Timed Petri Nets Transforming to Timed Automata
摘要
Abstract
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网/时间自动机Key words
formal verification,model checking,Petri nets,timed automata分类
信息技术与安全科学引用本文复制引用
邓小妮,罗雪山..向时间自动机转换的军事电子信息系统性质验证[J].火力与指挥控制,2011,36(12):134-137,4.基金项目
武器装备基金资助项目(51406010704KG0143) （51406010704KG0143）
