| 基于Event-B的联锁进路控制建模验证方法研究 |
| |
| 引用本文： | 童湖东,宁滨,王海峰.基于Event-B的联锁进路控制建模验证方法研究[J].铁路计算机应用,2013,22(6):57-61. |
| |
| 作者姓名： | 童湖东 宁滨 王海峰 |
| |
| 作者单位： | 北京交通大学轨道交通控制与安全国家重点实验室,北京,100044%北京交通大学轨道交通运行控制系统国家工程研究中心,北京,100044 |
| |
| 摘 要： | 计算机联锁系统具有典型的安全苛求特性.传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证.本文利用形式化Event-B方法和相关工具对联锁系统的核心功能-进路控制的相关功能需求和安全需求进行了建模、精化和验证,对开发高安全苛求和高可靠性的联锁软件提供了新的方法借鉴.
|
| 关 键 词： | 联锁 进路控制 Event-B建模 形式化方法 |
| 收稿时间： | 2013-06-15 |
Research on Event-B based modeling and verification of interlocking route control |
| |
| TONG Hudong
,
NING Bin
,
WANG Haifeng.Research on Event-B based modeling and verification of interlocking route control[J].Railway Computer Application,2013,22(6):57-61. |
| |
| Authors: | TONG Hudong NING Bin WANG Haifeng |
| |
| Institution: | 1.State Key Laboratory of Rail Traffic Control and Safety,Beijing Jiaotong University,Beijing 100044,China; 2.National Engineering Research Centre of Rail Transportation Operation and Control System,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Abstract: | |
| |
| Keywords: | interlocking route control Event-B modeling formalization method |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《铁路计算机应用》浏览原始摘要信息 |
| 点击此处可从《铁路计算机应用》下载免费的PDF全文 |
|
