10.13682/j.issn.2095-6533.2015.05.011
基于Spin的地铁门控制系统建模与验证
针对地铁门控制系统(MDCS)安全问题,提出一种 MDCS 检测方法。通过分析 MDCS 的控制逻辑,使用Promela建立了基于 Spin的 MDCS系统模型,将 MDCS中的地铁控制系统、地铁门控制系统及屏蔽门控制系统抽象为三个进程,并用线性时态逻辑公式描述待验证性质,运行 Spin后即可判断 MDCS是否存在安全隐患。实验结果表明,该检测方法可有效验证 MDCS的安全性。
地铁门控制系统、模型检测、Spin、Promela
TP301(计算技术、计算机技术)
国家自然科学基金资助项目61050003;陕西省教育厅自然科学基金资助项目11JK1037
2015-09-29(万方平台首次上网日期,不代表论文的发表时间)
共5页
57-61