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 261kB |
Official URL: https://doi.org/10.1007/978-3-030-85248-1_10
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.
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: | |
Statistics: | download |
Deposited On: | 14 Sep 2021 14:50 |
Repository Staff Only: item control page