Verifying the Mathematical Library of a UAV Autopilot with Frama-C

Abstract

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 paper presents an ongoing work on the formal verification of the Paparazzi UAV autopilot using the Frama-C verification platform. We focus on a Paparazzi mathematical library providing different UAV state representations and associated conversion functions and manage to prove the absence of runtime errors in the library and some interesting functional properties on floating-point conversion functions.

Date
Aug 24, 2021 2:30 PM
Event
FMICS 2021
Location
Videoconference
Baptiste Pollien
Baptiste Pollien
PhD Student in Formal Methods

My research interests focus on formal methods applied for UAV Autopilot.