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

Abstract

Lors du développement de système critique, comme 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.

Baptiste Pollien, PhD

Software Engineer HMI

I am a Software Engineer HMI at Ampere Software Technology.