首页 | 本学科首页   官方微博 | 高级检索  
     

基于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
Affiliation: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 万方数据 等数据库收录!
点击此处可从《铁路计算机应用》浏览原始摘要信息
点击此处可从《铁路计算机应用》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号