原文传递
铁路信号联锁系统安全规范的形式化描述与验证方法
| 论文题名： | 铁路信号联锁系统安全规范的形式化描述与验证方法 |
| 关键词： | 铁路信号;联锁系统;安全规范;形式化描述;验证方法 |
| 摘要： | 铁路信号的根本功能是保障列车运行安全、提高运输效率，车站联锁系统是铁路信号的核心技术装备，它通过对信号机、道岔和进路的控制来指挥行车、防止列车冲突。随着计算机联锁系统的应用推广，联锁系统对软件的依赖性越来越强，如何提高联锁软件的质量、确保系统安全是近年来轨道交通领域研究的热点问题。联锁系统安全规范的严格描述与验证对保障软件开发质量具有重要意义。 本文从我国铁路信号联锁逻辑控制电路入手，深入分析提炼联锁系统的安全规范，利用形式化方法进行严格的描述与分析验证，具体工作如下: 1.查阅大量文献，论文首先对形式化方法在铁路领域的应用进行了深入的分析和综述，阐述了联锁系统开发过程存在的规范表达二义性和不精确问题; 2.结合形式化方法的发展趋势，研究了普适性形式化规格描述与验证方法，并对当前流行的方法进行了分类总结，深入探讨了Event-B方法。 3.深入研究了6502电气集中联锁逻辑控制电路，结合站场图，重点分析了信号开放控制、四线制道岔控制电路、进路建立和分段解锁等联锁关键环节，提炼出关键环节的联锁系统的安全规范。利用逻辑语义和一阶谓词逻辑对安全规范进行了形式化描述。 4.结合具体的站场实例，基于Event-B方法，利用Rodin平台，对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析，给出了严格的分析结果。 工作表明，铁路信号联锁系统是具有复杂时序逻辑的控制系统，Event-B方法适合于该类系统的描述与验证。通过形式化的联锁安全规范描述与验证，可以在系统开发的早期及时发现设计错误或漏洞，有助于提高计算机联锁系统的软件开发质量。本文的工作，为现阶段我国铁路信号安全关键软件的开发提供了借鉴。 |
| 作者： | 张越 |
| 专业： | 交通信息工程与控制 |
| 导师： | 王海峰 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2013 |
| 正文语种： | 中文 |
检索历史
应用推荐
