基于有色Petri网的电梯门系统建模与仿真  

Modeling and Simulation of Elevator Door System Based on Colored Petri Net

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

机构地区：[1]南京航空航天大学自动化学院,江苏南京210016

出　　处：《计算机技术与发展》2015年第3期162-166,共5页Computer Technology and Development

基　　金：国家自然科学基金资助项目(60674100)

摘　　要：文中分析了电梯门系统的组成结构,描述了电梯门系统的运行过程。文中利用有色Petri网中不同颜色的token可以表示系统的不同类型的状态的原理建立了基于有色Petri网的电梯门系统模型,避免了传统Petri网建模模型时引起的状态空间爆炸问题。然后利用CPN Tools对模型进行动态分析并生成状态空间报告以分析模型的回归性、有界性、活性及公平性。活性分析存在死标识时,提出基于ASK-CTL模型检验理论的死标识合理性算法验证模型中不存在自循环终端和死锁标识,进而验证了死标识存在的合理性,证实了电梯门系统CPN模型的正确性。It has analyzed the composition and structure of the elevator door system,and has described the operating process of the elevator door system. Apply the theory that the Colored Petri Net（ CPN） can express different states of a system with different color of the token to establish an elevator door system model which is based on CPN,which avoids the state space explosion of the traditional Petri Net.Then use the CPN Tools to analyze the models automatically and generate the state space report to analyze its home properties,boundedness properties,liveness properties and fairness properties. When existing dead marking by liveness analyzing,propose reasonable algorithm proving model of dead marking based on ASK-CTL to verify that the model exists no self loop terminals and deadlock markings,which proves reasonable existence of the dead markings and the correction of the CPN model of the elevator door system.

关 键 词：电梯门系统 有色PETRI网 ASK-CTL 死标识 活性 

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