没有合适的资源?快使用搜索试试~ 我知道了~
论文研究-车站联锁进路控制逻辑的形式化方法.pdf
需积分: 10 0 下载量 163 浏览量
2019-09-11
06:23:58
上传
评论
收藏 599KB PDF 举报
温馨提示
试读
6页
基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化 方法Event-B为基础,引入角色Agent对联锁系统进行规范定义,通过智能体与Event-B的建模和验证,构造了车站联锁进路控制逻辑形式化验证模型,并进行 了形式化规范和推理,该模型在RODIN平台上进行验证,通过实例验证,满足了计算机联锁系统的安全需求。
资源推荐
资源详情
资源评论
2016,52(17)
1 引言
计算机联锁系统
[1]
是铁路及城市轨道交通信号系统
中极重要的子系统,是为了保证行车安全,提高铁路运
输效率,改善行车人员劳动条件的重要技术装备。为了
保证车站行车安全,在信号、道岔和进路之间必须保持
一定的制约关系和工作顺序,将这种制约关系和工作顺
序称为联锁
[2]
,计算机联锁系统主要是利用联锁软件完
成联锁功能的。联锁是个过程,这个过程也就是进路控
制过程。
车站联锁控制直接关系到行车安全,也影响到车站
作业的效率及行车组织工作,因此联锁系统在不断改
进。传统的联锁软件开发主要应用于软件工程的需求
分析方法,在设计、分析和测试上已无法满足计算机联
锁系统的安全需求。在过去的几年里,类似推理的多智
能体系统中也有成功的规范出现,王铁江
[3]
等提出了一
种 Z 规格说明,显著提高了计算机联锁软件的质量,并
也有利于将来对其进行更严格的测试;Hansen
[4]
等采用
VDM(Vienna Development Method,维也纳开发方法)
车站联锁进路控制逻辑的形式化方法
胡晓辉
1
,韩佳芮
2
HU Xia ohui
1
, HAN Jiarui
2
1.兰州交通大学 电子与信息工程学院,兰州 7 30070
2.兰州交通大学 图书馆,兰州 730070
1.School of Electronic & Information Engineering, Lanzho u Jiaotong University, La nzhou 730070, China
2.Library of Lanzhou Jiaoton g University, Lanzhou 730070, China
HU Xiaohui, HAN Jiarui. Route contr ol station interlock logic of formal methods. Compu ter Engineering and
Applicatio ns, 2016 , 52(17):229-234.
Abstract:A computer-based interlocking sys tem is one pair of train travel system to provide safe conditions for the sys-
tem, the station interlock system is to ensure that the station traffic safety and i mprove transport efficiency of a typical
safety-cr itical system. In this paper, based o n the formal method Event-B, it introduces the role of Agent interlock system
specification defines, thr ough modelin g and verifying agent and Event-B, it constructs the station interlocking route con-
trol log ic formal verifica tion 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 对联锁系统进行规范定义,通过
智能体与 Ev ent-B 的建模和验证,构造了车站联锁进路控制逻辑形式化验证模型,并进行了形式化规范和推理,该模
型在 RODIN 平台上进行验证,通过实例验证,满足了计算机联锁系统的安全需求。
关键词:联锁;进路控制;Event-B 方法;多智能体系统(MAS)
文献标志码:A 中图分类号:TP391.9;U283 doi:10.3778/j.issn.1002-8331.1409-0283
⦾工程与应用⦾
基金项目:国家自然科学基金(No.61163009);甘肃省硕导项目(No.1104 -05)。
作者简介:胡晓辉(1963—),男,博士,教授,研究领域为智能信息处理、分布式计算;韩佳芮(1988—),女,硕士研究生,研究领域
为软件形式化,E-mail:hanjiarui@ 163.com。
收稿日期:2014-09-19 修回日期:2015-03-02 文章编号:1002-833 1(2016)17-0229-06
CNKI 网络优先出版:2015-04-21, http://www.cnki.net/kcms/detail/11.2127.TP.20150421. 1028.035.html
C omputer Enginee ring and Applications 计算机工程与应用
229
资源评论
weixin_38744153
- 粉丝: 346
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功