Formal Verification of an UAV autopilot: Static analysis and Verified Code Generation

Abstract

Critical systems are systems whose failure could have catastrophic consequences, such as the destruction of expensive equipment or the death of people. These systems are found in the automotive, medical and drone autopilot systems. It is essential to ensure that these systems do not present a risk of failure. Formal methods are powerful verification techniques for obtaining strong guarantees on such systems, even if it is generally not possible to formally verify the entire system. This thesis deals with the formal verification of certain critical software components of a drone autopilot. It made it possible to review different methods of verification and proof of programs that can be applied to such software and use them on a case study, the Paparazzi autopilot developed at ENAC.

Baptiste Pollien, PhD

Software Engineer HMI

I am a Software Engineer HMI at Ampere Software Technology.