| 基于Uppaal的时延Petri网到时间自动机等价模型验证* |
| |
| 引用本文： | 周清雷,王静. 基于Uppaal的时延Petri网到时间自动机等价模型验证*[J]. 计算机应用研究, 2005, 22(6): 64-66 |
| |
| 作者姓名： | 周清雷 王静 |
| |
| 作者单位： | 1. 郑州大学,信息工程学院,河南,郑州,450052;信息工程大学,信息工程学院,河南,郑州,450002
2. 郑州大学,信息工程学院,河南,郑州,450052 |
| |
| 基金项目： | 国家自然科学基金资助项目（69873040） |
| |
| 摘 要： | 时延Petri网和时间自动机都可以有效地对实时系统的行为进行模拟和性能分析。利用时延Petri网到时间自动机等价转换算法（简记作TPN-to-TA 转换），将一个描述实时系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型。使用时间自动机中成熟的模型验证工具Uppaal对此时延Petri网的模型进行验证。
|
| 关 键 词： | 时延Petri网；时间自动机；TPN-to-TA转换；Uppaal |
| 文章编号： | 1001-3695(2005)06-0064-03 |
| 修稿时间： | 2004-04-27 |
Model Checking of Timed Petri Nets to Semantically Equivalent Timed Automata Based on Uppaal |
| |
| ZHOU Qing-lei,WANG Jing. Model Checking of Timed Petri Nets to Semantically Equivalent Timed Automata Based on Uppaal[J]. Application Research of Computers, 2005, 22(6): 64-66 |
| |
| Authors: | ZHOU Qing-lei WANG Jing |
| |
| Affiliation: | (1.School of Information Engineering,Zhengzhou University, Zhengzhou Henan 450052, China; 2.School of Information Engineering, Information Engineering University, Zhengzhou Henan 450002, China) |
| |
| Abstract: | Both timed Petri nets and timed automata can carry on behavior simulation and performance analysis to the real-time system effectively.Utilizes a translation algorithm (referred to as TPN-to-TA translation) which can map a timed Petri nets model of real-time system into a collect of semantically equivalent timed automata, use a mature model checker Uppaal for timed automata to verify the performance of this timed Petri nets model. |
| |
| Keywords: | Timed Petri Nets Timed Automata TPN-to-TA Translation Uppaal |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用研究》浏览原始摘要信息 |
|
点击此处可从《计算机应用研究》下载全文 |
