Projet Hi-Lite : AdaCore veut révolutionner la vérification des logiciels critiques

Hi-Lite est un projet de recherche piloté par AdaCore, un fournisseur de solutions logicielles commerciales pour Ada (un langage de programmation de pointe pour concevoir des applications critiques).

Dans ce cadre, cet éditeur, qui se développe entre l’Europe et les Etats-Unis, est associé à des partenaires comme Thales, Altran, EADS-Astrium, l’INRIA, et le CEA List.

Les résultats du projet ont été présentés à Paris la semaine dernière avec toutes les parties prenantes. ITespresso y était.

Quel est le but poursuivi par Hi-Lite ? Démocratiser l’utilisation des méthodes formelles dans le développement des logiciels critiques (des logiciels complexes dont dépendent des personnels ou moyens de grandes valeurs) qui sont notamment très importants dans les systèmes embarqués de l’aviation ou de l’aérospatiale.

Fondamentalement, une méthode formelle est une preuve mathématique, comme on les apprend au lycée.

Les logiciels reposent sur un grand nombre de programmes développés à partir d’algorithmes mathématiques très complexes (dans le cas des logiciels critiques).

Or toute formule mathématique (ou ce qui en dépend) peut être prouvé. Et si le programme est prouvé, c’est qu’il est fiable et ne peut pas connaître de bugs.

Le problème de cette méthode de vérification formelle, c’est qu’il faut posséder de grandes connaissances à la fois mathématiques et techniques pour être capable de développer les preuves dont on se sert.

Les développeurs  de ces logiciels critiques ne sont pas tous des titulaires de thèses. Alors il faut simplifier l’approche des langages de programmation comme Ada.

C’est tout l’enjeu du programme de recherche Hi-Lite :  permettre aux développeurs de logiciels critiques dépourvus de compétences mathématiques poussées de se servir des preuves dans un environnement de programmation qui leur est familier.

En trois ans, AdaCore et ses partenaires ont développé deux nouveaux outils permettant aux langages Ada et C de prendre en charge les preuves formelles.

Il s’agit de SPARK Pro pour le premier et Frama-C pour le deuxième.

Ils permettent au programmeur d’écrire le code de son logiciel puis d’accéder par de simples boutons aux programmes de preuves inclus dans les outils d’Hi-Lite.

Ces derniers scannent le code écrit et toutes ses formules et les comparent aux preuves mathématiques censées démontrer le fonctionnement du logiciel.

Après ce scan apparaissent différentes informations suivant un code couleur : rouge (problème), vert (tout va bien), et d’autres particularités similaires à n’importe quel environnement de programmation.

L’avantage, c’est que ces preuves éprouvent le code source du logiciel à un niveau encore jamais atteint jusqu’alors avec les méthodes de vérifications classiques (un test pour un cas d’application particulier).

Il existe un point noir dans cette démarche.

Etant donné que ce sont des programmes tiers qui effectuent les preuves mathématiques, qu’arriverait-il à l’ensemble des logiciels vérifiés à l’aide de méthodes formelles si ces programmes étaient eux-même bogués ?

Yannick Moy, développeur pour AdaCore, répond : « En théorie, si les preuves sont boguées, tous les logiciels vérifiés ne peuvent être certifiés. Cela remet en question tout le gain de fiabilité. Cela implique que nous ne pourrons jamais totalement nous passer des tests classiques, ils seront dans un premier temps associés aux méthodes formelles. »

Après le projet Hi-Lite, la phase de commercialisation

Pour l’aboutissement du projet Hi-Lite, AdaCore s’est appuyé sur 5 partenaires.

Le projet s’est d’abord vu labellisé par le pôle de compétitivité System@tic.

Ce qui lui a permis d’obtenir des subventions d’Etat et des collectivités territoriales (1,4 million d’euros sur les 3,9 qu’aura coûté le projet) ainsi que de profiter des relations professionnelles du pôle.

« System@tic a été essentiel pour le lancement de ce projet. Un pôle de compétitivité est une association d’entreprises réunies autour de secteurs et d’enjeux économiques bien définis par cette association », déclare Romain Berrendonner, Directeur juridique et responsable du montage et du suivi des projets de recherche du pôle de compétitivité System@tic.

« Lorsque nous soutenons des programmes de recherches comme Hi-Lite, cela crédibilise leurs qualités et leurs potentiels, de sorte que l’Etat peut les financer en toute connaissance de cause. »

Il ajoute : « la réussite d’un projet dépend aussi beaucoup de la taille de son équipe. Il faut savoir affecter la bonne quantité de personnes (ou d’entreprises) à un projet pour profiter de l’étendue de leurs connaissances sans pour autant rendre impossible la communication entre les différents acteurs de la recherche. »

De ce point de vue-là, AdaCore a su organiser l’équipe de Hi-Lite. La PME a amené ses connaissances du langage Ada et développé SPARK.

L’institut CEA List a apporté ses connaissances du langage C et développé Frama-C.

Les chercheurs de l’INRIA ont quant à eux mis au point les programmes effectuant les vérifications formelles.

Le trio THALES – Altran et EADS-ASTRIUM a contribué au projet de recherche en fournissant quantité de cas pratiques permettant aux chercheurs du projet Hi-Lite d’appliquer leur solution à de nombreux domaines : avionique, aérospatiale, etc.

Le projet maintenant achevé et opérationnel, AdaCore et ses associés se préparent à commercialiser la solution.

A l’avenir, ils comptent associer SPARK et Frama-C pour pouvoir appliquer les preuves formelles à des logiciels encore plus complexes utilisant les deux langages Ada et C.

Après avoir démarré le projet Hi-Lite avec 25 employés, AdaCore termine la phase de test avec 10 collaborateurs supplémentaires.

L’éditeur est consciente que sa solution intéressera de nombreuses entreprises dans le domaine de l’aviation et de l’aérospatial.

« Notre compréhension du potentiel d’Hi-Lite n’a pas cessé d’évoluer en même temps que nous travaillions dessus », affirme Jamie Ayre, directeur marketing d’AdaCore.

« Comme les logiciels courants deviennent de plus en plus complexes, il est possible que demain, même l’automobile, la médecine ou la téléphonie soient intéressés par les méthodes formelles. Elles sauveront même des vies. »

En attendant que les clients se découvrent, d’autres acteurs viendront peut-être concurrencer AdaCore sur son terrain.

En effet, pour démontrer sa compétitivité et profiter de connaissances extérieures, l’équipe d’Hi-Lite a choisi de rendre accessible sur Internet tout ce qui a été développé en open source.

La première adresse se trouve via OpenDo Forge et l’autre via Frama-C.

Une initiative originale qui ne manquera certainement pas d’intriguer la communauté des développeurs d’applications critiques.

Présentation du projet Hi-Lite menée en 2011 par Yannick Moy pour l’Initiative de Recherche et Innovation sur le Logiciel Libre (IRILL)

————–

Connaissez-vous le logiciel libre ?

————–

Credit photo :Shutterstock.com –  Copyright : Michelangelus