OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Vérification d’une bibliothèque mathématique d’un autopilote avec Frama-C

Pollien, Baptiste Vérification d’une bibliothèque mathématique d’un autopilote avec Frama-C. (2021) In: Approches formelles dans l'assistance au développement de logiciels - AFADL 2021, 16 June 2021 - 18 June 2021 (Virtual event, France).

[img]
Preview
(Document in English)

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

Official URL: http://www.lirmm.fr/afadl2021/docs/actes-afadl2021.pdf

Abstract

Lors du développement de système critiques, comme par exemple un autopilote de drone, il est essentiel de s’assurer que le programme est sûr, en utilisant par exemple des méthodes formelles. Pour faciliter la vérification, on se restreint généralement à une abstraction du système ou un sous-ensemble. Cet article présente la vérification d’une bibliothèque mathématique de l’autopilote Paparazzi, à l’aide de l’outil Frama-C, afin de garantir l’absence d’erreur à l’exécution et certaines propriétés fonctionnelles.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-03274906
Audience (conference):National conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Laboratory name:
Statistics:download
Deposited On:30 Jun 2021 13:20

Repository Staff Only: item control page