No Cover Image

Journal article 600 views

Techniques for modelling and verifying railway interlockings / Phillip James; Faron Moller; Hoang Nga Nguyen; Markus Roggenbach; Steve Schneider; Helen Treharne

International Journal on Software Tools for Technology Transfer, Volume: 16, Issue: 6, Pages: 685 - 711

Swansea University Author: Moller, Faron

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1007/s10009-014-0304-7

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

Full description

Published in: International Journal on Software Tools for Technology Transfer
Published: 2014
URI: https://cronfa.swan.ac.uk/Record/cronfa20836
Tags: Add Tag
No Tags, Be the first to tag this record!
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.
Item Description: Originality:This paper proposes and develops rigorous mathematical ideas which are original. In particular, the decomposition strategy ("covering") is wholly new and undoubtedly the greatest of the abstraction techniques. Two other techniques considered in this paper, finitisation and topological abstraction, have been explored (by us) earlier, but are further extended in this paper.Significance:This paper describes work which is carried out in the context of a research project with Siemens Rail Automotive UK, and the experimental results described in this paper demonstrate a significant reduction in the times required to verify real-world railway scheme plans provided by Siemens.Rigour:Software Tools for Technology Transfer is a leading journal from a highly respected academic publisher (Springer-Verlag) with stringent refereeing criteria ensuring that only work recognised as internationally-excellent is accepted.
College: College of Science
Issue: 6
Start Page: 685
End Page: 711