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.
Specification and verification of railway safety-critical systems using TLA+: A Case Study / Salierno, Giulio; Morvillo, Sabatino; Leonardi, Letizia; Cabri, Giacomo. - (2020). (Intervento presentato al convegno 29th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises WETICE 2020 tenutosi a Basque Coast - Bayonne, France nel 2020).
Specification and verification of railway safety-critical systems using TLA+: A Case Study
Giulio Salierno;Letizia Leonardi;Giacomo Cabri
2020
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
Specification_and_verification_of_railway_safety-critical_systems_using_TLA_A_Case_Study.pdf
Accesso riservato
Tipologia:
VOR - Versione pubblicata dall'editore
Licenza:
[IR] publisher-specific-oa
Dimensione
707.77 kB
Formato
Adobe PDF
|
707.77 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris