CAJ | 학술논문

针对使用 CPN Tools 工具建立系统 CPN（Colored Petri Net）模型并进行仿真所得到的状态空间报告中出现的死标识是否会影响系统的安全性和模型的正确性进行研究，提出基于 ASK-CTL 的有色 Petri 网模型检验算法及死标识合理性验证算法。算法描述了系统有色 Petri 网的建模与仿真过程，根据得到的状态空间报告判断是否存在死标识，对存在的死标识采用非标准状态空间查询法使用 ML 语言编辑相关功能函数以验证死标识的合理性，进而确保所建立 CPN 模型的正确性与系统的安全性。最后，以电梯门系统为例，证明了算法的有效性。
침대사용 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.