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

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

基于Event-B的计算机联锁安全规范描述与验证

本文结合具体的站场实例,基于Event-B方法对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析,给出了严格的分析结果.工作表明,铁路信号联锁系统是具有复杂时序逻辑的控制系统,Event-B方法适合于该类系统的描述与验证.通过形式化的联锁安全规范描述与验证,可以在系统开发的早期及时发现设计错误或漏洞,有助于提高计算机联锁系统的软件开发质量.