基于精确标识对象Petri网模型的检测方法  

The Methods for Verifying PNO with Precisemarking Model

作　　者：张红军[1,2] 卢红星[2] 叶阳东[2] 

机构地区：[1]河南省政法管理干部学院计算机科学系 [2]郑州大学信息工程学院

出　　处：《河南科学》2006年第6期881-885,共5页Henan Science

基　　金：河南省自然科学基金资助项目(0411012300)

摘　　要：精确标识PNO要求一个对象实例既不能同时出现在多个库所,也不能在一个托肯中出现多次,SMV是一个功能强大的符号化模型检验工具.本文提出了将精确标识PNO模型转换成相应SMV程序的算法,并通过列车运行区域模型(TOPNO)演示了具体的转换过程.通过该转换算法不仅能有效地解决精确标识PNO活性、安全性等属性的检测问题,还能验证与模型中对象相关的属性.PNO with precise marking is a kind of PNO in which the same object neither occur in more than one place at the same time nor occur more than one times in the same token. SMV is a powerful symbol verification tool. This paper present an algorithm for transfer a PNO model with precise marking into a SMV program, and demonstrates the process through a case of Train Operation Petri Net with Objects （TOPNO）. The case show that we can not only solves the problem effectively for verifying the properties such as safety and liveness of a PNO with precise marking model through the algorithm, but also solves the problem for verifying the properties of objects in the model.

关 键 词：带有对象的Petri网 精确标识 SMV 模型验证 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]