TITLE

Techniques for modelling and verifying railway interlockings

AUTHOR(S)
James, Phillip; Moller, Faron; Nguyen, Hoang; Roggenbach, Markus; Schneider, Steve; Treharne, Helen
PUB. DATE
November 2014
SOURCE
International Journal on Software Tools for Technology Transfer;Nov2014, Vol. 16 Issue 6, p685
SOURCE TYPE
Academic Journal
DOC. TYPE
Article
ABSTRACT
We describe a novel framework for modelling railway interlockings which has been developed in conjunction with railway engineers. The modelling language used is CSP $$||$$ B. Beyond the modelling we present a variety of abstraction techniques which make the analysis of medium- to large-scale networks feasible. The paper notably introduces a covering technique that allows railway scheme plans to be decomposed into a set of smaller scheme plans. The finitisation and topological abstraction techniques are extended from previous work and are given formal foundations. All three techniques are applicable to other modelling frameworks besides CSP $$||$$ B. Being able to apply abstractions and simplifications on the domain model before performing model checking is the key strength of our approach. We demonstrate the use of the framework on a real-life, medium-size scheme plan.
ACCESSION #
98882884

 

Share

Read the Article

Courtesy of THE LIBRARY OF VIRGINIA

Sorry, but this item is not currently available from your library.

Try another library?
Sign out of this library

Other Topics