No Cover Image

Conference Paper/Proceeding/Abstract 537 views

Defining and model checking abstractions of complex railway models using CSP||B / Faron, Moller

Haifa Verification Conference 2012

Swansea University Author: Faron, Moller

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 c...

Full description

Published in: Haifa Verification Conference 2012
Published: Berlin Heidelberg Springer Verlag 2013
Online Access: http://www.cs.swan.ac.uk/~csfm/hvc12.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa13711
Tags: Add Tag
No Tags, Be the first to tag this record!
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.
Keywords: formal methods, model checking, railway verification
College: College of Science