计算机应用与软件
計算機應用與軟件
계산궤응용여연건
Computer Applications and Software
2015年
10期
302-305,333
,共5页
马国富%刘文良%周建勇%刘久富
馬國富%劉文良%週建勇%劉久富
마국부%류문량%주건용%류구부
模型检验%死标识%电梯门系统%CPN 模型
模型檢驗%死標識%電梯門繫統%CPN 模型
모형검험%사표식%전제문계통%CPN 모형
Model checking%DeadMarkins%Elevator door system%CPN model
针对使用 CPN Tools 工具建立系统 CPN(Colored Petri Net)模型并进行仿真所得到的状态空间报告中出现的死标识是否会影响系统的安全性和模型的正确性进行研究,提出基于 ASK-CTL 的有色 Petri 网模型检验算法及死标识合理性验证算法。算法描述了系统有色 Petri 网的建模与仿真过程,根据得到的状态空间报告判断是否存在死标识,对存在的死标识采用非标准状态空间查询法使用 ML 语言编辑相关功能函数以验证死标识的合理性,进而确保所建立 CPN 模型的正确性与系统的安全性。最后,以电梯门系统为例,证明了算法的有效性。
針對使用 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.