|
|||||
|
|
| 基于精确标识对象Petri网模型的检测方法 | |
| 作者姓名： | 张红军 卢红星 叶阳东 |
| 作者单位： | 河南省政法管理干部学院,计算机科学系,郑州,450002;郑州大学,信息工程学院,郑州,450052;郑州大学,信息工程学院,郑州,450052 |
| 摘 要： | 精确标识PNO要求一个对象实例既不能同时出现在多个库所,也不能在一个托肯中出现多次,SMV是一个功能强大的符号化模型检验工具.本文提出了将精确标识PNO模型转换成相应SMV程序的算法,并通过列车运行区域模型(TOPNO)演示了具体的转换过程.通过该转换算法不仅能有效地解决精确标识PNO活性、安全性等属性的检测问题,还能验证与模型中对象相关的属性. |
| 关 键 词： | 带有对象的Petri网 精确标识 SMV 模型验证 |
| 文章编号： | 1004-3918(2006)06-0881-05 |
| 收稿时间： | 2006-05-26 |
| 修稿时间： | 2006-05-26 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |