| 基于精确标识对象Petri网模型的检测方法 |
| |
| 引用本文： | 张红军,卢红星,叶阳东.基于精确标识对象Petri网模型的检测方法[J].河南科学,2006,24(6):881-885. |
| |
| 作者姓名： | 张红军 卢红星 叶阳东 |
| |
| 作者单位： | 1. 河南省政法管理干部学院,计算机科学系,郑州,450002;郑州大学,信息工程学院,郑州,450052
2. 郑州大学,信息工程学院,郑州,450052 |
| |
| 摘 要： | 精确标识PNO要求一个对象实例既不能同时出现在多个库所,也不能在一个托肯中出现多次,SMV是一个功能强大的符号化模型检验工具.本文提出了将精确标识PNO模型转换成相应SMV程序的算法,并通过列车运行区域模型(TOPNO)演示了具体的转换过程.通过该转换算法不仅能有效地解决精确标识PNO活性、安全性等属性的检测问题,还能验证与模型中对象相关的属性.
|
| 关 键 词： | 带有对象的Petri网 精确标识 SMV 模型验证 |
| 文章编号： | 1004-3918(2006)06-0881-05 |
| 收稿时间： | 2006-05-26 |
| 修稿时间： | 2006年5月26日 |
The Methods for Verifying PNO with Precisemarking Model |
| |
| ZHANG Hong-jun,LU Hong-xing,YE Yang-dong.The Methods for Verifying PNO with Precisemarking Model[J].Henan Science,2006,24(6):881-885. |
| |
| Authors: | ZHANG Hong-jun LU Hong-xing YE Yang-dong |
| |
| Institution: | 1. Department of Computer Science, Henan Administrative Institute of Politics and Law, Zhengzhou 450002, China; 2. The Information Engineering of Zhengzhou University, Zhengzhou 450052, China |
| |
| Abstract: | 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. |
| |
| Keywords: | SMV |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
