+ formal "/>

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

2020 IEEE 29th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE)(2020)

Cited 1|Views12
No score
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.
Translated text
Key words
Railway software specification,Verification,Validation,Formal methods
AI Read Science
Must-Reading Tree
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined