Bas Luttik: Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 toolset

Event Details

ERTMS Hybrid Level 3 is a recent proposal for a train control system specification that serves to increase the capacity of the railway network by allowing multiple trains on a single track section.

We have formally modelled and analysed the principles of ERTMS Hybrid Level 3 in mCRL2.

Our analysis has resulted in suggestions for improvement of the principles that will be taken into account in the next version of the specification.

In this talk I’ll introduce ERTMS Hybrid Level 3, I’ll discuss how we have obtained an mCRL2 model (or actually several mCRL2 models) for it, and I’ll report on and explain some of the results of our analysis.

(Based on joint work with Maarten Bartholomeus and Tim Willemse.)