Interlocking Design Automation Using Prover Trident

摘要

This article presents the industrial-strength Prover Trident approach to develop and check safety-critical interlocking software for railway signaling systems. Prover Trident is developed by Prover Technology to meet industry needs for reduced cost and time-to-market, by capitalizing on the inherent repetitive nature of interlocking systems, in the sense that specific systems can be created and verified efficiently as specific instances of generic principles. This enables a high degree of automation in an industrial-strength toolkit for creation of design and code, with seamless integration of push-button tools for simulation and formal verification. Safety assessment relies on formal verification, performed on the design, the revenue service software code as well as the binary code, using an independent toolset for formal verification developed to meet the applicable certification requirements. Basic ideas of this approach have been around for some time [1, 2, 3], while methodology and tools have matured over many industrial application projects. The presentation highlights the main ingredients in this successful application of formal methods, as well as challenges in establishing this approach for production use in a conservative industry domain.