Notwithstanding the large amount of attempts to formally verify them, railway interlocking systems still represent a challenging problem for automatic verification. Interlocking systems controlling sufficiently large stations, due to their inherent complexity related to the high number of variables involved, are not readily amenable to automatic verification, typically incurring in state space explosion problems. The study described in this paper aims at evaluating and experimenting the industrial application of verification by model checking for this class of systems. The choices made at the beginning of the study, also on the basis of specific requirements from the industrial partner, are presented, together with the advancement status of the project and the plans for its completion.

Validation of Railway Interlocking Systems by Formal Verification, A Case Study / Andrea, Bonacchi; Alessandro, Fantechi; Stefano, Bacherini; Matteo, Tempestini; Leonardo, Cipriani. - STAMPA. - 8368:(2014), pp. 237-252. (Intervento presentato al convegno International Conference on Software Engineering and Formal Methods SEFM 2013: Software Engineering and Formal Methods) [10.1007/978-3-319-05032-4_18].

Validation of Railway Interlocking Systems by Formal Verification, A Case Study

BONACCHI, ANDREA;FANTECHI, ALESSANDRO;
2014

Abstract

Notwithstanding the large amount of attempts to formally verify them, railway interlocking systems still represent a challenging problem for automatic verification. Interlocking systems controlling sufficiently large stations, due to their inherent complexity related to the high number of variables involved, are not readily amenable to automatic verification, typically incurring in state space explosion problems. The study described in this paper aims at evaluating and experimenting the industrial application of verification by model checking for this class of systems. The choices made at the beginning of the study, also on the basis of specific requirements from the industrial partner, are presented, together with the advancement status of the project and the plans for its completion.
2014
Lecture Notes in Computer ScienceSoftware Engineering and Formal Methods
International Conference on Software Engineering and Formal Methods SEFM 2013: Software Engineering and Formal Methods
Andrea, Bonacchi; Alessandro, Fantechi; Stefano, Bacherini; Matteo, Tempestini; Leonardo, Cipriani
File in questo prodotto:
File Dimensione Formato  
chp%3A10.1007%2F978-3-319-05032-4_18.pdf

Accesso chiuso

Tipologia: Pdf editoriale (Version of record)
Licenza: Tutti i diritti riservati
Dimensione 350.34 kB
Formato Adobe PDF
350.34 kB Adobe PDF   Richiedi una copia

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

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/845321
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 6
social impact