OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

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

Pollien, Baptiste and Garion, Christophe and Hattenberger, Gautier and Roux, Pierre and Thirioux, Xavier Verifying the Mathematical Library of an UAV Autopilot with Frama-C. (2021) In: Formal Methods for Industrial Critical Systems - FMICS 2021, 24 August 2021 - 26 August 2021 (Paris, France).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/978-3-030-85248-1_10


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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Part of the Lecture Notes in Computer Science book series (LNCS, volume 12863) Also part of the Programming and Software Engineering book sub series (LNPSE, volume 12863)
HAL Id:hal-03344191
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Ecole Nationale de l'Aviation Civile - ENAC (FRANCE)
Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE)
Laboratory name:
Deposited On:14 Sep 2021 14:50

Repository Staff Only: item control page