摘要
基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化方法 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.
作者
胡晓辉
韩佳芮
HU Xiaohui;HAN Jiarui(School of Electronic & Information Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China;Library of Lanzhou Jiaotong University, Lanzhou 730070, China)
出处
《计算机工程与应用》
CSCD
北大核心
2016年第17期229-234,270,共7页
Computer Engineering and Applications
基金
国家自然科学基金(No.61163009)
甘肃省硕导项目(No.1104-05)
