Ensuring safety of critical systems is crucial and is often attained by extensive testing of the system. Formal methods are now commonly accepted as powerful tools to obtain guarantees on such systems, even if it is generally not possible to formally prove the safety and correctness of the whole system. This thesis deals with the formal verification of some software components of an autopilot. These components have been selected according to their criticality and should therefore be correct by construction and/or by verification. The goal of this thesis is first to review the formal verification and program proof methods that can be applied to such software in order to apply them on these components of the Paparazzi autopilot developed at ENAC. This thesis also aims to see if the analysis process using such techniques and associated tools can be applied on projects that already exist and are not designed for the verification tools. This thesis focuses on two techniques for the verification of two specific components of Paparazzi.
The first component is a Paparazzi mathematical library verified using the Frama-C platform. This library provides different UAV state representations and associated conversion functions that are used by the drone control system in order to take flight decisions. The Frama-C platform is used with the WP, EVA and RTE plugins to verify the absence of runtime errors in the library and some interesting functional properties on floating-point conversion functions. This verification work required the specification of the correctness properties in the form of function contracts (pre and post condition). The majority of the contracts were automatically verified by the SMT solvers except for some functional properties that must be manually helped using the Coq proof assistant.
The second component verified is a flight plan generator. Paparazzi has a domain specific language called FPL, used to specify flight plans. It is a programming and modelling language allowing the expression of complex missions. FPL missions are compiled into C code that is directly embedded into the autopilot code. The FPL to C code generator, currently written in OCaml, is therefore a critical component when addressing the drone safety. This thesis formally verifies the FPL compilation process. First, three-pass code generator, targeting the Clight intermediate language from the CompCert suite has been developed in Coq. Then, an operational semantics have been formally defined. Finally, the generator has been formally verified by manually proving a bisimulation relation between FPL semantics and Clight semantics. In the course of the formalization and verification process, we have also unveiled several problems in the original Paparazzi code generator.