基于Event-B的联锁进路控制建模验证方法研究

• 作者: 宁滨 王海峰 童湖东
• 来源期刊: 铁路计算机应用
• 学科: 交通运输
• 关键词: 联锁 进路控制 Event-B建模 形式化方法
• 年，卷（期）: 2013,（6）
• 所属期刊栏目: 计算机与通信信号
• 页码范围: 57-61
• 页数: 5页
• 分类号: U284.3|TP39
• 字数: 2279字
• 语种: 中文

摘要

计算机联锁系统具有典型的安全苛求特性.传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证.本文利用形式化Event-B方法和相关工具对联锁系统的核心功能-进路控制的相关功能需求和安全需求进行了建模、精化和验证,对开发高安全苛求和高可靠性的联锁软件提供了新的方法借鉴.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	宁滨	北京交通大学轨道交通控制与安全国家重点实验室	82	815	18.0	26.0
2	王海峰	北京交通大学轨道交通运行控制系统国家工程研究中心	31	313	10.0	17.0
3	童湖东	北京交通大学轨道交通控制与安全国家重点实验室	1	7	1.0	1.0