文献类型：期刊文献

中文题名：基于精确标识对象Petri网模型的检测方法

英文题名：The Methods for Verifying PNO with Precisemarking Model

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

第一作者：张红军

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

第一机构：河南财经政法大学计算机与信息工程学院

年份：2006

卷号：24

期号：6

起止页码：881-885

中文期刊名：河南科学

外文期刊名：Henan Science

收录：CSTPCD

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

语种：中文

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

外文关键词：petri net with objects; precise marking; SMV; model verification

摘要：精确标识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.