On the validation of an interlocking system by model-checking
Bonacchi A, Fantechi A
Model checking D.2.4 Software/Program Verification. Formal methods Interlocking systems Railway Signalling Systems
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.
Metrics
Back to previous page
@inproceedings{oai:it.cnr:prodotti:305300,
title = {On the validation of an interlocking system by model-checking},
author = {Bonacchi A and Fantechi A},
doi = {10.1007/978-3-319-10702-8_7},
year = {2014}
}
0000-0002-4648-4667