Specification and verification of railway safety-critical systems using TLA+: A Case Study
Giulio Salierno, Sabatino Morvillo, Letizia Leonardi, Giacomo Cabri · 2020
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.