车站联锁进路控制逻辑的形式化方法

计算机工程与应用 ›› 2016, Vol. 52 ›› Issue (17): 229-234.

车站联锁进路控制逻辑的形式化方法

胡晓辉1，韩佳芮2

1.兰州交通大学电子与信息工程学院，兰州 730070
2.兰州交通大学图书馆，兰州 730070

出版日期:2016-09-01 发布日期:2016-09-14

Route control station interlock logic of formal methods

HU Xiaohui1, HAN Jiarui2

1.School of Electronic & Information Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China
2.Library of Lanzhou Jiaotong University, Lanzhou 730070, China

Online:2016-09-01 Published:2016-09-14

摘要/Abstract

摘要： 基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统，车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化方法Event-B为基础，引入角色Agent对联锁系统进行规范定义，通过智能体与Event-B的建模和验证，构造了车站联锁进路控制逻辑形式化验证模型，并进行了形式化规范和推理，该模型在RODIN平台上进行验证，通过实例验证，满足了计算机联锁系统的安全需求。

关键词: 联锁, 进路控制, Event-B方法, 多智能体系统（MAS）

Abstract: A computer-based interlocking system is one pair of train travel system to provide safe conditions for the system, the station interlock system is to ensure that the station traffic safety and improve transport efficiency of a typical safety-critical system. In this paper, based on the formal method Event-B, it introduces the role of Agent interlock system specification defines, through modeling and verifying agent and Event-B, it constructs the station interlocking route control logic formal verification model, and conducts a formal specification and reasoning, the model is verified on the RODIN platform, validating by example, it meets the security needs of computer interlocking system.

Key words: interlock, route control, event-b method, Multi-Agent System（MAS）

胡晓辉1，韩佳芮2. 车站联锁进路控制逻辑的形式化方法[J]. 计算机工程与应用, 2016, 52(17): 229-234.

HU Xiaohui1, HAN Jiarui2. Route control station interlock logic of formal methods[J]. Computer Engineering and Applications, 2016, 52(17): 229-234.

[1]	秦发园1，戴胜华1，徐昱2. 进路建立过程的时间有色petri网建模与仿真[J]. 计算机工程与应用, 2015, 51(8): 266-270.
[2]	张昱，徐洪泽，陈建强，张鹿宁. 冶金企业内部铁路进路控制优化策略研究[J]. 计算机工程与应用, 2015, 51(17): 250-254.
[3]	胡晓辉，王振强，陈永. 车-地通信场景的一种混合建模方法研究[J]. 计算机工程与应用, 2015, 51(16): 228-233.
[4]	张舒青，徐中伟，陈祖希. 基于项重写系统的联锁系统模型检测方法研究[J]. 计算机工程与应用, 2014, 50(3): 49-54.
[5]	石擎宇，谭丽，成利刚. 基于图论的联锁程序的研究与设计[J]. 计算机工程与应用, 2013, 49(21): 46-50.
[6]	张友鹏，权海宁. 新型分布式全电子计算机联锁系统研究[J]. 计算机工程与应用, 2012, 48(24): 187-191.
[7]	郭荣佐^1，2，黄君³，王霖². 嵌入式联锁控制器软件体系结构动态建模研究[J]. 计算机工程与应用, 2010, 46(2): 213-217.
[8]	祝庚^1,2. 联锁进路生成的切换控制算法设计[J]. 计算机工程与应用, 2009, 45(16): 208-210.
[9]	刘臣勇¹,周颖^2,3. 人工干预条件下多媒体联锁仿真研究[J]. 计算机工程与应用, 2007, 43(35): 213-215.
[10]	杜军威,徐中伟,王树梅. 联锁逻辑模型的安全性分析[J]. 计算机工程与应用, 2007, 43(2期): 1-1.
[11]	杜军威徐中伟. 基于时序Petri网的联锁逻辑形式建模与验证[J]. 计算机工程与应用, 2007, 43(13): 7-10.