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）

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

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