University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Defining and model checking abstractions of complex railway models using CSP||B

Moller, F, Nguyen, HN, Roggenbach, M, Schneider, S and Treharne, H (2013) Defining and model checking abstractions of complex railway models using CSP||B Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7857 L. pp. 193-208.

Available under License : See the attached licence file.

Download (371kB)
Text (licence)

Download (33kB)


The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios. © 2013 Springer-Verlag Berlin Heidelberg.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Moller, F
Nguyen, HN
Roggenbach, M
Schneider, S
Treharne, H
Date : 2013
DOI : 10.1007/978-3-642-39611-3-20
Additional Information : The original publication is available at
Depositing User : Symplectic Elements
Date Deposited : 21 Oct 2013 11:06
Last Modified : 20 Dec 2014 02:33

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800