PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ferrari A., Magnani G., Grasso D., Fantechi A. Model checking interlocking control tables. In: FORMS/FORMAT 2010 - Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 (Braunschweig, Germany, 2-3 December 2010). Proceedings, vol. 2 pp. 107 - 115. Eckehard Schnieder, Geza Tarnai. Springer, 2011.
 
 
Abstract
(English)
A challenging problem for model checking is represented by railway interlocking systems. It is a well known fact that interlocking systems, due to their inherent complexity related to the high number of variables involved, are not amenable to automatic verifi cation, typically incurring in state space explosion problems. The literature is however quite scarce on data concerning the size of interlocking systems that have been successfully proved with model checking techniques. In this paper we attempt a systematic study of the applicability bounds for general purpose model checkers on this class of systems, by studying the typical characteristics of control tables and their size parameters. The results con firm that, although small scale interlocking systems can be addressed by model checking, interlockings that control medium or large railway yards cannot, asking for specialized verifi cation techniques.
URL: http://www.springerlink.com/content/j5318h232646410w/
DOI: 10.1007/978-3-642-14261-1_11
Subject Formal Methods
Interlocking
Control Table Verification
Model Checking
NuSMV
SPIN
D.2 SOFTWARE ENGINEERING
D.2.4 Software/Program Verification


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