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

• 作者: 卢红星 叶阳东 张红军
• 来源期刊: 河南科学
• 关键词: 带有对象的Petri网 精确标识 SMV 模型验证
• 年，卷（期）: 2006,（6）
• 页码范围: 881-885
• 页数: 5页
• 分类号: TP301.1
• 语种: 中文
• DOI: 10.3969/j.issn.1004-3918.2006.06.027

摘要

精确标识PNO要求一个对象实例既不能同时出现在多个库所,也不能在一个托肯中出现多次,SMV是一个功能强大的符号化模型检验工具.本文提出了将精确标识PNO模型转换成相应SMV程序的算法,并通过列车运行区域模型(TOPNO)演示了具体的转换过程.通过该转换算法不仅能有效地解决精确标识PNO活性、安全性等属性的检测问题,还能验证与模型中对象相关的属性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	叶阳东	郑州大学信息工程学院	69	612	14.0	22.0
2	张红军	河南省政法管理干部学院计算机科学系	5	10	2.0	3.0
6	卢红星	郑州大学信息工程学院	14	19	2.0	3.0