| 基于Petri网的一种时序分析方法 |
| |
| 引用本文： | 傅建明,朱福喜,彭蓉.基于Petri网的一种时序分析方法[J].小型微型计算机系统,2000,21(4):368-371. |
| |
| 作者姓名： | 傅建明 朱福喜 彭蓉 |
| |
| 作者单位： | 1. 国家多媒体软件工程技术研究中心、教育部多媒体软件开放研究实验室,武汉,430072
2. 武汉大学计算机科学及技术学院,武汉,430072 |
| |
| 摘 要： | Ｐｅｔｒｉ网由于有强大的建模能力和成熟的理论支持，被广泛应用于各种系统的建模．本文通过把Ｐｅｔｒｉ网转换成转移系统，利用转移系统和Ｋｒｉｐｋｅ结构给出时序逻辑语义的解释，从而建立了一种在Ｐｅｔｒｉ网上进行时序分析的方法．这种方法是根据不动点理论，用模型检查验证公式正确性．通过对Ａｄａ程序会合性质进行模型检查，验证了这种方法的有效性．
|
| 关 键 词： | Petri网 转移系统 时序分析 模型检查 |
A TEMPORAL ANALYSIS METHOD OF PETRI-NETS BASED |
| |
| FU Jian-ming,ZHU Fu-xi,PENG Rong.A TEMPORAL ANALYSIS METHOD OF PETRI-NETS BASED[J].Mini-micro Systems,2000,21(4):368-371. |
| |
| Authors: | FU Jian-ming ZHU Fu-xi PENG Rong |
| |
| Abstract: | Analysis and verification of concurrent program is a hotspot of research.Petri net models many systems because of its power model ability and its mature theory,but Petri net can not express some property which temporal formulae can express well. We map reachable state graph of Petri net to transition system,and give interpretation of temporal logic semantics according to transition system and Kripke structure,furthermore develop a temporal analysis method on Petri net with Model checking.Finally,We demonstrate this method validity via checking rendezvous correctness of Ada. |
| |
| Keywords: | Petri net Transition system Temporal logic Model checking Fix Point |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
