Specification and verification of railway safety-critical systems using TLA+: A Case Study

In this paper, we describe our experience in using the TLA+ formal language for modelling and analysis of a concrete scenario from the railway domain. A train status alert system has been specified and verified using the TLA+ by formally verifying abstract specifications of the real system. The verification of TLA+ models enabled us to detected ambiguity in machine transitions before implementing the real system. A translation algorithm is proposed to produce relay logic from the state-machine model in order to verify interlocking components. Our contribution helps to integrate formal methods into existing railway development process without needing to update the legacy railway computer-based systems.