论文部分内容阅读
联锁系统是铁路信号系统的重要组成部分，直接关系到车站行车和作业的安全与效率。计算机联锁系统由于具有高效、智能化、易于维护的优点而成为当前联锁系统运用的主流。联锁软件是计算机联锁系统正确执行联锁运算、实现联锁功能的关键，必须具备极高的安全性和可靠性。当前的联锁软件开发主要使用传统的基于软件工程的方法，在需求定义上难以保证完备性和一致性，仿真和测试也不足以完整分析和验证软件安全性，容易形成安全隐患，同时，开发出的软件可维护性不高。 本文针对传统联锁软件开发方法存在的问题，从实际应用角度出发提出基于Event-B的形式化解决方案，选取联锁软件核心功能——进路控制进行了形式化建模和验证的探索研究，主要研究工作如下: (1)分析了当前联软件开发方法存在的缺陷和引入形式化解决方案的可能性，研究了Event-B形式化建模验证方法的理论基础和应用特点，介绍了Event-B方法相关工具，提出了基于Event-B的联锁软件形式化开发方法。 (2)分析了联锁软件进路控制具体流程，在此基础上制定了联锁进路控制Event-B模型的建立步骤和精化策略，并根据制定的步骤和精化策略，在Rodin工具平台下借助UML-B工具逐步建立了包含进路选排、信号控制、进路锁闭、自动解锁和人工解锁各进程功能需求和安全需求的进路控制Event-B模型。 (3)采用模型仿真和模型证明相结合的方法对建立的联锁进路控制Event-B模型进行了形式化验证，其中模型仿真部分采用了UML-B状态机仿真的方法，模型证明部分则借助Event-B证明义务机制和Rodin平台采用了自动证明和交互式证明相结合的方法，结果表明本文所建立的进路控制模型能覆盖系统功能需求和安全需求，模型有效性、正确性和一致性能得到完整验证。 本文的研究结果表明，基于Event-B的形式化建模验证方法能准确和有效的描述联锁进路控制的功能需求和安全需求，并且完整的分析和验证模型安全特性，能运用于联锁软件开发中以增强软件安全性并提高开发效率。