In this talk, I will discuss our recent experiences with using the mCRL2 toolset – which has a process-algebra based modelling language, a modal mu-calculus-based property language, and an explicit-state model checker – to support two major innovation activities from railway infrastructure managers.
First, there is the EULYNX initiative of the European railway infrastructure managers. The aim of EULYNX is to standardise the interfaces between the interlocking and field elements (signals, points, level crossings); these interface standards are modelled in SysML. In a project funded by the Dutch and German railway infrastructure managers we are translating the SysML models to mCRL2 not only to formally assess the quality of the standard by model checking, but also to facilitate using them for model-based testing of compliance to the standard of delivered components.
Second, in collaboration with the Dutch railway infrastructure manager ProRail we have formally modelled and analysed the ERTMS Hybrid Level 3 principles. These principles facilitate subdividing track sections into virtual subsections, in order to allow multiple trains simultaneously on the same track section, thus increasing capacity. We have plans to support ProRail developers in their further elaboration of the design and implementation of ERTMS Hybrid Level 3.