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.

Preview	Text hvc2012_usbpreproceedings.pdf Available under License : See the attached licence file. Download (371kB)
Preview	Text (licence) SRI_deposit_agreement.pdf Download (33kB)

Abstract

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 :	Name Email ORCID 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 http://www.springerlink.com
Depositing User :	Symplectic Elements
Date Deposited :	21 Oct 2013 11:06
Last Modified :	20 Dec 2014 02:33
URI:	http://epubs.surrey.ac.uk/id/eprint/796018

Actions (login required)

View Item

Downloads