DOI 10.1007/s10009-014-0304-7 FMRCS Techniques for modelling and verifying railway interlockings

Abstract We describe a novel framework for modelling railway interlockings which has been developed in conjunc-tion 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 intro-duces a covering technique that allows railway scheme plans to be decomposed into a set of smaller scheme plans. The fini-tisation and topological abstraction techniques are extended from previous work and are given formal foundations. All three techniques are applicable to other modelling frame-works besides CSP||B. Being able to apply abstractions and simplifications on the domain model before perform-ing model checking is the key strength of our approach. We demonstrate the use of the framework on a real-life, medium-size scheme plan