Mark Bouwman: Verification and model-based testing of a railway point/switch using mCRL2

Event Details

The EULYNX initiative is a collaborative effort of more than ten European railway infrastructure managers to standardise signalling interfaces. Within EULYNX, FormaSig aims to use formal methods to analyse the correctness of the standard. We have recently concluded a case study in which we translate the EULYNX Point interface from SysML to mCRL2. The resulting mCRL2 model is subsequently used to contribute to the quality of the standard by verifying whether important safety requirements hold for the model. Test cases have been automatically derived from the same mCRL2 model. They have been executed, effectively checking whether an actual Point implementation conforms to the EULYNX standard. This talk will discuss the case study itself and the lessons learned concerning formalising SysML and applying formal methods in the railway domain.