PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bonacchi A., Fantechi A. On the validation of an interlocking system by model-checking. In: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference (Florence, Italy, 11-12 September 2014). Proceedings, pp. 94 - 108. Frédéric Lang, Francesco Flammini (eds.). (Lecture Notes in Computer Science, vol. 8718). Springer-Verlag, 2014.
 
 
Abstract
(English)
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.
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-10702-8_7#page-1
DOI: 10.1007/978-3-319-10702-8
Subject Railway Signalling Systems
Interlocking systems
Model checking
D.2.4 Software/Program Verification. Formal methods


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional