The Application of Formal Methods to Railway Signalling Software

Laurent Voisin

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.

About Laurent Voisin

Laurent Voisin received an engineering degree from ENSTA ParisTech. He started his carrier in the Software Engineering department of Steria Group (developing compilers and IDE) before switching to formal methods in the mid 90s.Since then, he has been a strong advocate of the use of formal methods in industry, both as a practitioner and tool developer, first at ClearSy, then Systerel. In 2004-2007, he took a sabbatical at ETH Zurich where he led the development of the open-source RODIN platform for formal system modelling.His current research interests revolve around the practical application of formal methods in the daily practice of software engineers, mainly in the railway domain.

Sponsored by

Official Media Partners

Supported by