基于Spin的地铁门控制系统建模与验证  

Spin based modeling and validation of metro door control system

作　　者：舒新峰[1] 张炎龙 孙林泽 

机构地区：[1]西安邮电大学计算机学院,陕西西安710121

出　　处：《西安邮电大学学报》2015年第5期57-61,共5页Journal of Xi’an University of Posts and Telecommunications

基　　金：国家自然科学基金资助项目(61050003);陕西省教育厅自然科学基金资助项目(11JK1037)

摘　　要：针对地铁门控制系统(MDCS)安全问题,提出一种MDCS检测方法。通过分析MDCS的控制逻辑,使用Promela建立了基于Spin的MDCS系统模型,将MDCS中的地铁控制系统、地铁门控制系统及屏蔽门控制系统抽象为三个进程,并用线性时态逻辑公式描述待验证性质,运行Spin后即可判断MDCS是否存在安全隐患。实验结果表明,该检测方法可有效验证MDCS的安全性。A checking method of MDCS is proposed to solve the safety problem existing in metro door control system （MDCS）. A system model with Promela is constructed based on the analysis of control logic of MDCS, the metro control system, the doors control system. A platform screen door control system is abstracted for the three processes from the MDCS, the properties to be verified are described by Linear Temporal Logic formulas, and the verification result of MDCS is obtained for any existing safety risks. Experiment result show that the proposed approach can be effectively used to verify the safety of the MDCS.

关 键 词：地铁门控制系统 模型检测 SPIN PROMELA 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]