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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
