Qinghai Tibet, China
Automated Simulation and Formal Verification of Interlocking Software
As part of a project for the Ministry of Railways of the People’s Republic of China, GE Transportation supplied 20+ interlocking systems for the Qinghai-Tibet railway. Prover Technology joined this project to specify the signaling rules governing test and safety principles for these systems, implemented on VHLC hardware controllers. These test and safety principles were used by GE Transportation to perform automated simulation and formal verification of the interlocking software using the Prover iLock Simulator and Prover iLock Verifier.
Following the success of this project, GE Transportation proceeded to incorporate support for Prover iLock in the VHLC programming tool ACE, so that interlocking software developed with Prover iLock can be imported into ACE.