基于 ASK-CTL 的有色 Petri 网模型检验算法研究

• 作者: 刘久富 刘文良 周建勇 马国富
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 模型检验 死标识 电梯门系统 CPN 模型
• 年，卷（期）: 2015,（10）
• 所属期刊栏目: 算 法
• 页码范围: 302-305,333
• 页数: 5页
• 分类号: TP391.9
• 字数: 4841字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2015.10.072

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	马国富	安阳工学院信息工程系	13	21	2.0	4.0
2	刘久富	南京航空航天大学自动化学院	53	207	8.0	11.0
3	刘文良	南京航空航天大学自动化学院	6	19	3.0	4.0
4	周建勇	南京航空航天大学自动化学院	8	22	3.0	4.0