基于Petri网的一种时序分析方法

A TEMPORAL ANALYSIS METHOD OF PETRI NETS BASED

Petri网由于有强大的建模能力和成熟的理论支持 ,被广泛应用于各种系统的建模 .本文通过把 Petri网转换成转移系统 ,利用转移系统和 Kripke结构给出了时序逻辑语义的解释 ,从而建立一种在 Petri网上进行时序分析的方法 .这种方法是根据不动点理论 ,用模型检查验证公式正确性 .通过对 Ada程序会合性质进行模型检查 。

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.