The 4SECURail formal methods demonstrator

The need for high-quality standard interfaces is widely recognized as a mandatory step to reduce procurement costs and create safely operating complex railway infrastructures. That is why European initiatives like EULYNX have been set up precisely with the purpose of supporting standard interfaces development. The exploitation of formal methods during the phase of standardization plays an essential role in raising the quality of the generated specifications. 4SECURail is a recent project that aims to precisely show, with a structured evaluation (known as the formal methods demonstrator), how formal methods might help to improve the quality of a specific signalling interface selected as case study. This paper describes the experience gained with the experiment.