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

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

针对使用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.