The Application of Formal Methods to Railway Signalling Software
R&D Manager, Systerel
Formal methods bring the rigour of mathematics to the analysis, development and verification of software. They provide the means to demonstrate that a design fulfills its specifications and are particularly helpful for the developement of high integrity software.
In this talk, I will reflect back on 20 years of experience of practicing formal methods for railway signalling software. I will firstly present a brief overview of some of the techniques available and where to apply them. I will then insist on the need for appropriate tooling. Finally, I will present how these techniques have been put into practice in an industrial safety-critical project of substantial size and will give some of the lessons learned during the last decade.