Centre de recherche Saclay - Île-de-France

Why3

Why3

Un langage pour la vérification déductive de programmes

La vérification d’un programme par preuve formelle consiste à transformer simultanément le code source et son comportement attendu en un ensemble d’énoncés mathématiques : les obligations de preuve. Il s’agit ensuite d’établir la véracité de ces énoncés à l’aide de logiciels de démonstration automatiques ou semi-automatiques. Cette méthode réduit le temps des tests et donc les coûts de la vérification.

Why3 est une boîte à outils pour la preuve mathématique de programmes, applicable à la vérification de systèmes critiques. Elle permet de prouver formellement qu’un code a le comportement attendu.

L’originalité de Why3 réside dans son adaptabilité, lui permettant d’être intégré dans différents logiciels pour la vérification de systèmes embarqués : il peut disposer de plusieurs langages d’entrées (C, Java, Ada, OCaml) et est capable d’exploiter de nombreux prouveurs en sortie (automatiques et/ou interactifs).

Fiche technique

Industrie
Défense & sécurité
Outils multidomaines

Une collaboration réussie

Why3 a, par exemple, été intégrée au cœur de l’environnement SPARK*, développé par la société AdaCore**, pour la vérification de codes critiques écrits en langage Ada. Cette intégration s’est déroulée dans le cadre du LabCom ProofInUse entre l’équipe Toccata et AdaCore.

Aujourd’hui, les projets clients SPARK ont des applications aussi variées que :

• les systèmes de gestion de trafic aérien
• la mise en œuvre à haute fiabilité de composants de véhicule
• le développement de logiciel embarqué fiable pour la santé (cœur artificiel de la société Scandinavian Real Heart AB)

La technologie Why3 est également utilisée dans d’autres environnements: Frama-C pour l’analyse de codes critiques écrits en langage C, développé au CEA-LIST ; TIS-Analyzer pour l’analyse également de codes C, développé par la PME TrustInSoft ; et dans un outil pour la vérification de PLC (Programmable Logic Controllers) développé par Mitsubishi Electric R&D Centre Europe.

 

* SPARK : Technologie de vérification formelle
** Adacore : PME éditrice de logiciels spécialisée dans la fourniture d’outils de développement pour les systèmes critiques

 

Démonstration de Why3

Tester le logiciel

 

La vidéo suivante présente une introduction à l’activité de preuve formelle et à l’utilisation de Why3 :

 

  • Lorsque nous avons cherché en 2010 à moderniser notre outil d’analyse formelle de programmes, nous nous sommes naturellement tournés vers l’équipe Toccata qui développait déjà l’outil Why et qui avait montré son avance scientifique et sa maturité technologique lors d’expériences d’adoption industrielle réussies. Le choix fait par l’équipe Toccata de développer des logiciels sous licence libre et leur soutien continu aux utilisateurs industriels ont été déterminants dans le succès de cette aventure commune.

    Cyrille Comar,
    Président d’AdaCore 

L'équipe Toccata

Ils nous font confiance