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

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. Ce talk 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

Baptiste Pollien, PhD

Software Engineer HMI

I am a Software Engineer HMI at Ampere Software Technology.