|
|||||
|
|
| 基于ASK-CTL的有色Petri网模型检验算法研究 | |
| 作者单位： | ;1.安阳工学院信息工程系;2.南京航空航天大学自动化学院 |
| 摘 要： | 针对使用CPN Tools工具建立系统CPN(Colored Petri Net)模型并进行仿真所得到的状态空间报告中出现的死标识是否会影响系统的安全性和模型的正确性进行研究,提出基于ASK-CTL的有色Petri网模型检验算法及死标识合理性验证算法。算法描述了系统有色Petri网的建模与仿真过程,根据得到的状态空间报告判断是否存在死标识,对存在的死标识采用非标准状态空间查询法使用ML语言编辑相关功能函数以验证死标识的合理性,进而确保所建立CPN模型的正确性与系统的安全性。最后,以电梯门系统为例,证明了算法的有效性。 |
| 关 键 词： | 模型检验 死标识 电梯门系统 CPN模型 |
STUDY ON COLOURED PETRI NET MODEL CHECKING BASED ON ASK-CTL |
|
| Abstract: | |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ | |