Document - Model checking interlocking control tables

2011

Conference article Closed Access

Model checking interlocking control tables

Ferrari A., Magnani G., Grasso D., Fantechi A.

Interlocking Model Checking Formal Methods NuSMV Control Table Verification

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.

Source: Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 - FORMS/FORMAT 2010, pp. 107–115, Braunschweig, Germany, 2-3 December 2010

Publisher: Springer, Berlin Heidelberg, DEU

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:199290,
	title = {Model checking interlocking control tables},
	author = {Ferrari A. and Magnani G. and Grasso D. and Fantechi A.},
	publisher = {Springer, Berlin Heidelberg, DEU},
	doi = {10.1007/978-3-642-14261-1_11},
	booktitle = {Formal Methods for Automation and Safety in Railway and Automotive Systems 2010 - FORMS/FORMAT 2010, pp. 107–115, Braunschweig, Germany, 2-3 December 2010},
	year = {2011}
}