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

• 作者: 罗雪山 邓小妮
• 来源期刊: 火力与指挥控制
• 学科: 工学
• 关键词: 形式化验证 模型检验 Petri网 时间自动机
• 年，卷（期）: 2011,（12）
• 所属期刊栏目: 工程实践
• 页码范围: 134-137
• 分类号: TP311
• 字数: 4232字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-0640.2011.12.037

摘要

日益复杂的军事电子信息系统面临正确性验证挑战,形式化验证方法如模型检验技术成为必需.给出基于时间Petri网表示的军事电子系统模型PMES的定义,然后给出PMES模型转换为时间自动机网的步骤,利用已有的基于时间自动机的模型检验工具对系统性质进行验证;系统的性质要求用时序逻辑语言CTL或TCTL公式表示.雷达干扰机系统说明了该方法的实际应用效果.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗雪山	国防科技大学信息系统与管理学院	123	1054	17.0	23.0
2	邓小妮	国防科技大学人文与社会科学学院	7	11	1.0	3.0