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

Research on Event-B based modeling and verification of interlocking route control

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

Computer Interlocking System was a safety critical system. Traditional development method for interlocking software couldn＇t ensure the completeness and safety of software function. The all errors couldn＇t be found by test. This paper used Event-B formalization method and relative tools to build models for the core function of interlocking---concerning its function requirement and safety requirement of route control, refined and proved the models. This method provided a new way of developing interlocking software.