The European Railway Traffic Management System has the purpose to provide a common signaling system for all the European nations. It consists of two subsystems: the trackside subsystem (TSS) and the on-board subsystem (OBS) that communicate to exchange information about the state of the trackside and/or the train. Radio communication can take place according to the requirements specification reported in ERTMS/ETCS SUBSET-026-3. As the communication between TSS and OBS is a critical issue, we exploit model checking to verify the correctness of the communication process as specified in the SUBSET-026-3. The results achieved during the experimentation seem to be very promising.

Formal Verification of Radio Communication Management in Railway Systems Using Model Checking Technique

Borrelli A.;Di Lucca G. A.;Nardone V.;
2019-01-01

Abstract

The European Railway Traffic Management System has the purpose to provide a common signaling system for all the European nations. It consists of two subsystems: the trackside subsystem (TSS) and the on-board subsystem (OBS) that communicate to exchange information about the state of the trackside and/or the train. Radio communication can take place according to the requirements specification reported in ERTMS/ETCS SUBSET-026-3. As the communication between TSS and OBS is a critical issue, we exploit model checking to verify the correctness of the communication process as specified in the SUBSET-026-3. The results achieved during the experimentation seem to be very promising.
2019
978-1-7281-0676-2
Formal methods; model checking; railway system; safety critical system
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

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