论文研究 车站联锁进路控制逻辑的形式化方法.pdf

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