Qinghai Tibet, China

Automated Simulation and Formal Verification of Interlocking Software

Purpose

Deploy state of the art safety verification, and to reduce recurring engineering costs for projects that deliver many interlocking systems

Infrastructure Manager

Ministry of Railways, PR China

Signaling system

VHLC, by General Electric

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.