Railway interlocking systems still represent a challenge for formal verification by model checking: the high number of complex interlocking rules that guarantee the safe movements of independent trains in a large station makes the verification of such systems typically incur state space explosion problems. In this paper we describe a study aimed to define a verification process based on commercial modelling and verification tools, for industrially produced interlocking systems, that exploits an appropriate mix of environment abstraction, slicing and CEGAR-like techniques, driven by the low-level knowledge of the interlocking product under verification, in order to support the final validation phase of the implemented products. © 2014 Springer International Publishing.
CITATION STYLE
Bonacchi, A., & Fantechi, A. (2014). On the validation of an interlocking system by model-checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8718 LNCS, pp. 94–108). Springer Verlag. https://doi.org/10.1007/978-3-319-10702-8_7
Mendeley helps you to discover research relevant for your work.