铁路信号联锁系统安全规范的形式化描述与验证方法

摘要

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

目录

声明

致谢

摘要

1 绪论

1．1 研究背景

1．2 铁路信号联锁系统的发展和问题

1．3 国内外研究现状

1．4 选题意义

1．5 论文研究内容及章节安排

2 形式化描述与验证方法

2．1 形式化方法

2．1．1 形式化描述

2．1．2 形式化验证

2．2 Event-B方法及Rodin平台

2．2．1 Event-B基本结构

2．2．2 Event-B数学体系

2．2．3 Event-B模型证明

2．2．4 Event-B模型的求精

2．2．5 Rodin平台

2．3 本章小结

3 联锁安全规范获取方法及逻辑语义描述

3．1 铁路信号联锁系统

3．2 联锁安全规范提取方法

3．2．1 进路控制安全规范

3．2．2 信号控制安全规范

3．2．3 道岔控制安全规范

3．3 联锁安全规范的逻辑语义描述

3．4 本章小结

4 基于Event-B的联锁系统安全规范的描述和验证

4．1 联锁系统安全规范Event-B描述方法

4．1．1 联锁安全规范的描述和精化策略

4．1．2 联锁安全规范的EVENT-B初始模型

4．1．3 联锁安全规范的Event-B模型的精化

4．2 联锁系统安全规范Event-B验证方法

4．3 本章小结

5 结论与展望

参考文献

附录 车站联锁Event-B初始模型

图目录

作者简历

学位论文数据集