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.
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.
|Divisions :||Faculty of Engineering and Physical Sciences > Computing Science|
|Identification Number :||https://doi.org/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|
Actions (login required)
Downloads per month over past year