Talk "Domain inherent abstractions for model checking within the railway domain"

by Markus Roggenbach

Fri, 10 January 2014 at 10:30 am in Theddingworth near Leicester, UK

Joint work with: P James, FG Moller, HN Nguyen, S Schneider, H Treharne

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 abstrac- tion 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.