有色Petri网模型中死标志合理性分析与验证

Analysis and verification of rationality of dead markings in colored Petri net models

针对使用CPN Tools对系统进行建模仿真得到的状态空间报告中出现的死标志是否会影响系统的安全性和模型的正确性进行了研究,提出了一种基于ASK-CTL及模型检验理论的死标志合理性验证算法。该算法采用模型检验技术通过ML语言编辑相关功能函数使用非标准状态空间查询法,进一步分析与研究CPN Tools仿真状态空间报告中出现的死标志,通过验证死标志存在的合理性来确保所建立CPN模型的准确性与系统的安全性。最后,以电梯门系统为例,使用CPN Tools建立电梯门系统的CPN模型,证明了算法的有效性。

To determinate that whether the deadmarkings affect the safety of the system and the correctness of the model or not in the state space report which obtained by using CPN Tools to simulate a CPN model,this paper proposed an algorithm which based on the ASK-CTL and model checking theories by using the non-standard state space query to verify the rationality of the deadmarkings in a CPN model. This algorithm was based on the theory of model checking and non-standard state space query which applied ML language to edit the functional functions would be obtained for a further study of the deadmarking in order to ensure the safety of the system or the correctness of the CPN model. Finally,it took an elevator door system as an example to verify the effectiveness of the proposed algorithm.