Use of Formal Proof for CBTC (OCTYS)
Christophe Tremblin, Pierre Lesoille, Omar Rezzoug · 2014
Ansaldo STS were pioneers in the introduction and use of innovative technologies such as High Speed systems, the European Railway Transportation Management System (ERTMS), PCC, Communications Based Train Control (CBTC) and driverless subway systems, with a permanent focus on safety, reliability, interoperability and performance. The desire for continuous improvement with regards to these criteria led Ansaldo STS to implement and evaluate formal proof techniques for software, with the aim of using these procedures on an industrial scale if they proved successful. This chapter concerns the implementation of these techniques over the course of the project, the pathways which were explored, the difficulties which had to be overcome and the feedback which led Ansaldo STS to extend the experiment to other projects and broaden the field of application of these formal methods.