基于ASK-CTL的有色Petri网模型检验算法研究  

STUDY ON COLOURED PETRI NET MODEL CHECKING BASED ON ASK-CTL

作　　者：马国富[1] 刘文良[2] 周建勇[2] 刘久富[2] 

机构地区：[1]安阳工学院信息工程系,河南安阳455000 [2]南京航空航天大学自动化学院,江苏南京210016

出　　处：《计算机应用与软件》2015年第10期302-305,333,共5页Computer Applications and Software

摘　　要：针对使用CPN Tools工具建立系统CPN(Colored Petri Net)模型并进行仿真所得到的状态空间报告中出现的死标识是否会影响系统的安全性和模型的正确性进行研究,提出基于ASK-CTL的有色Petri网模型检验算法及死标识合理性验证算法。算法描述了系统有色Petri网的建模与仿真过程,根据得到的状态空间报告判断是否存在死标识,对存在的死标识采用非标准状态空间查询法使用ML语言编辑相关功能函数以验证死标识的合理性,进而确保所建立CPN模型的正确性与系统的安全性。最后,以电梯门系统为例,证明了算法的有效性。To determinate whether or not the DeadMarkings in state space report,which is obtained from building and simulating a system CPN model with coloured Petri net （CPN）Tools,will affect the safety of the system and the correctness of the model,this paper proposes two algorithms：the CPN model checking algorithm based on ASK-CTL,and the rationality verification algorithm of DeadMarkings in CPN model. The first one describes the process of modelling and simulation of a system CPN,and judges the existence of the DeadMarkins according to the state space report.The second one uses non-standard state space query and ML language to edit the related functional functions to verify the rationality of existing DeadMarkings.Both of them are used to ensure the correctness of the CPN model built and the safety of system. Finally,an elevator door system is taken as an example to verify the effectiveness of the proposed algorithm.

关 键 词：模型检验 死标识 电梯门系统 CPN 模型 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]