Petri网模型的扩展与检测  

Extension and verification of Petri-net models

作　　者：姜洋[1] 罗贵明[1] 

机构地区：[1]清华大学软件学院,北京100084

出　　处：《计算机应用》2007年第1期183-185,共3页journal of Computer Applications

基　　金：清华大学基础研究基金资助项目(JCPY2005060);清华亚洲基金资助项目(2005B1)

摘　　要：扩展了基本Petri网,提出了更加适合模型检测的MCPN方法,并将MCPN模型转换成模型检测工具SPIN的输入语言———PROMELA。使用SPIN完成对系统模型的检测,以提高软件设计的可靠性。在转换过程中,考虑了对当前情态下处于激活状态的多个变迁的同时激发;并提出了一种处理Petri网公平性问题的解决方案。Petri-net is a precise mathematic model which is suitable to describe concurrency, synchronism and nondeterminism, and it has been widely used in the design of software/hardware systems. In this paper, we extended the basic simple Petri-net, advanced MCPN（ Petri-net for model checking） which is more suitable for model checking, and transformed MCPN models into PROMELA -- the input language of model checker SPIN. Then we can use the SPIN tools to do the model checking work in order to enhance the reliability of system design. We considered simultaneous firing of sets of transitions （Transitions in the set have no conflict with each other）. Also we developed a method to handle the fairness problem effectively. Finally our approach is exemplified by a case study.

关 键 词：PETRI网 模型检测 PROMELA 公平性 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论] TP311.52[自动化与计算机技术—计算机科学与技术]