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.
2020
29th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises WETICE 2020
Basque Coast - Bayonne, France
2020
Salierno, Giulio; Morvillo, Sabatino; Leonardi, Letizia; Cabri, Giacomo
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).
File in questo prodotto:
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

Licenza Creative Commons
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

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11380/1226051
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact