Journal article 606 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
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...
|Published in:||International Journal on Software Tools for Technology Transfer|
No Tags, Be the first to tag this record!
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.
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 of Science