| 向时间自动机转换的军事电子信息系统性质验证 |
| |
| 引用本文： | 邓小妮,罗雪山.向时间自动机转换的军事电子信息系统性质验证[J].火力与指挥控制,2011,36(12). |
| |
| 作者姓名： | 邓小妮 罗雪山 |
| |
| 作者单位： | 1. 国防科技大学人文与社会科学学院,长沙,410073
2. 国防科技大学信息系统与管理学院,长沙,410073 |
| |
| 摘 要： | 日益复杂的军事电子信息系统面临正确性验证挑战,形式化验证方法如模型检验技术成为必需.给出基于时间Petri网表示的军事电子系统模型PMES的定义,然后给出PMES模型转换为时间自动机网的步骤,利用已有的基于时间自动机的模型检验工具对系统性质进行验证;系统的性质要求用时序逻辑语言CTL或TCTL公式表示.雷达干扰机系统说明了该方法的实际应用效果.
|
| 关 键 词： | 形式化验证 模型检验 Petri网 时间自动机 |
Verification of Military Electronic Information Systems Based on Timed Petri Nets Transforming to Timed Automata |
| |
| DENG Xiao-ni
,
LUO Xue-shan.Verification of Military Electronic Information Systems Based on Timed Petri Nets Transforming to Timed Automata[J].Fire Control & Command Control,2011,36(12). |
| |
| Authors: | DENG Xiao-ni LUO Xue-shan |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
