The PERF Approach for Formal Verification

In order to analyse extensively the safety of the deployed railway software systems, RATP rely on rigorous verification methodologies based on formal methods. During the past few years, RATP has developed a new formal verification method called PERF, supported by a rich proof tool-chain. The main purpose of this method is to perform a non-intrusive verification on the implemented software. Unlike many formal methodologies, it does not require any intervention in the early stages of the software development. In this paper, we present the PERF methodology as well as the different part of its supporting tool-chain with some feedback on the its application in some real projects. We also present the ongoing and future work around the PERF tool-chain.