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 Springer International Publishing.
CITATION STYLE
Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M., & Cipriani, L. (2014). Validation of railway interlocking systems by formal verification, a case study. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8368 LNCS, pp. 237–252). Springer Verlag. https://doi.org/10.1007/978-3-319-05032-4_18
Mendeley helps you to discover research relevant for your work.