Document - On the validation of an interlocking system by model-checking

2014

Conference article Restricted

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.

Source: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference, pp. 94–108, Florence, Italy, 11-12 September 2014

Publisher: Springer, Berlin , Germania

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:305300,
	title = {On the validation of an interlocking system by model-checking},
	author = {Bonacchi A. and Fantechi A.},
	publisher = {Springer, Berlin , Germania},
	doi = {10.1007/978-3-319-10702-8_7},
	booktitle = {FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference, pp. 94–108, Florence, Italy, 11-12 September 2014},
	year = {2014}
}