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

Route control station interlock logic of formal methods

作　　者：胡晓辉[1] 韩佳芮[2] HU Xiaohui;HAN Jiarui(School of Electronic & Information Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China;Library of Lanzhou Jiaotong University, Lanzhou 730070, China)

机构地区：[1]兰州交通大学电子与信息工程学院,兰州730070 [2]兰州交通大学图书馆,兰州730070

出　　处：《计算机工程与应用》2016年第17期229-234,270,共7页Computer Engineering and Applications

基　　金：国家自然科学基金(No.61163009);甘肃省硕导项目(No.1104-05)

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

关 键 词：联锁 进路控制 Event-B方法 多智能体系统(MAS) 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术] U283[自动化与计算机技术—计算机科学与技术]