基于Event-B的计算机联锁安全规范描述与验证 |
| |
引用本文: | 张越,王海峰.基于Event-B的计算机联锁安全规范描述与验证[J].铁路计算机应用,2013,22(11):47-49,53. |
| |
作者姓名: | 张越 王海峰 |
| |
作者单位: | 北京交通大学轨道交通电子信息工程学院,北京,100044 |
| |
摘 要: | 本文结合具体的站场实例,基于Event-B方法对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析,给出了严格的分析结果.工作表明,铁路信号联锁系统是具有复杂时序逻辑的控制系统,Event-B方法适合于该类系统的描述与验证.通过形式化的联锁安全规范描述与验证,可以在系统开发的早期及时发现设计错误或漏洞,有助于提高计算机联锁系统的软件开发质量.
|
关 键 词: | 计算机联锁 安全规范 Event-B 形式化 规范验证 |
收稿时间: | 2013-11-15 |
本文献已被 维普 等数据库收录! |
| 点击此处可从《铁路计算机应用》浏览原始摘要信息 |
| 点击此处可从《铁路计算机应用》下载免费的PDF全文 |
|