Actualité

Méthode formelle de preuve de programme par la vérification déductive : technologies & cas d’usage des environnements Frama-C & SPARK

Publié le 20 mai 2019

# Fiabilité logicielle
# Systèmes à niveau critique de sûreté et sécurité

Garantir la haute intégrité des logiciels utilisés dans les systèmes demandant un niveau critique de sûreté est un enjeu majeur.
La vérification du code source est ainsi une étape cruciale du développement logiciel, afin de s’assurer de la correction fonctionnelle et de la sûreté du programme.

Si le test est une méthode largement standardisée dans l’industrie, il présente certains freins, notamment la difficulté de mise en œuvre et son caractère partiel.

D’autres méthodes, dites formelles, proposent une approche mathématique de la correction du logiciel par la preuve de programme.
Elles consistent en une analyse statique du code, par opposition aux analyses dynamiques qui nécessitent d’exécuter le code, comme le test de programme.

Frama-C & SPARK au programme de l’OSIS

Le 3 juin prochain, l’OSIS (Printemps de l’Innovation Open Source) s’intéressera à la vérification déductive qui est donc une méthode formelle de preuve de programme, et à deux de ses outils, Frama-C et SPARK.

La vérification déductive s’appuie en particulier sur les démonstrateurs, automatiques et interactifs, qui mécanisent les raisonnements logiques.

Frama-C, développé par le CEA et Inria, est une plateforme open source d’analyse statique du code C. Le langage de programmation C, bien que très difficile à maîtriser, est souvent choisi comme langage de prédilection pour la réalisation de systèmes demandant un niveau critique de sûreté. La validation du programme C dans ces systèmes est donc un enjeu d’autant plus important.

SPARK, développé par AdaCore, Altran et Inria, est à la fois un langage de programmation basé sur les méthodes formelles et dérivé du langage Ada, et une boite à outils de vérification déductive.

Un événement animé par des experts académiques et industriels internationaux

Le programme de l’événement Frama-C & SPARK Day 2019, co-organisé dans le cadre de l’OSIS par le CEA List, AdaCore, TrustInSoft et Inria, propose de faire le point sur les initiatives académiques et industrielles innovantes en matière d’analyse logicielle.

Des experts internationaux, chercheurs et tech lead, présenteront à cette occasion :

  • Des cas d’usage dans les secteurs de la conduite autonome, la santé, l’embarqué, l’IoT
  • Des retours d’expérience avec Altran, Thalès, Mitsubishi Electric, EasyMile
  • Des technologies innovantes : Why3, TrustInSoft Analyzer, uberSpark

Découvrir le programme

S'inscrire