Integrated formal verification of safety-critical software

This work presents a formal verification process based on the Systerel Smart Solver (S3) toolset for the development of safety-critical embedded software. In order to guarantee the correctness of the implementation of a set of textual requirements, the process integrates different verification techniques (inductive proof, bounded model checking, test cases generation, and equivalence proof) to handle different types of properties at their best capacities. It is aimed at the verification of properties at system, design, and code levels. To handle the floating-point arithmetic (FPA) in both the design and the code, an FPA library is designed and implemented in S3. This work is illustrated on an Automatic Rover Protection system implemented onboard a robot. Focus is placed on the verification of safety and functional properties and on the equivalence proof between the design model and the generated code.