D enombreux projets de R&D en développement logiciel, en électronique embarquée,pour des applications aéronautiques, etc. sont annoncés régulièrement dans la presse, avec force financements à la clé. Mais, une fois l'effervescence passée, on n'entend plus trop parler desdits projets. Ce ne fut pas le cas pour le projet open source Hi-Lite. L'éditeur AdaCore, spécialisé dans les solutions logicielles pour le langage Ada, a en effet annoncé l'aboutissement de ce projet auquel participaient aussi Altran, Astrium Space Transportation, CEA List, INRIA Toccata et Thales Communications. Financé notamment par Oséo et le Conseil général de l'Essonne, pour un budget global de 3,9 Me sur trois ans, le projet de recherche du pôle de compétitivité System@tic avait pour ambition de démocratiser les méthodes formelles dans le développement de logiciels critiques en associant la vérification formelle et les tests. Les systèmes critiques continuant à croître en taille et en complexité, les phases de développement et les budgets étant réduits, les tests deviennent une activité consommatrice de temps et de ressources, notamment lors de la conformité aux standards avioniques (norme sDO-178B et DO-178C). « Les objectifs du projet Hi-Lite étaient de rendre l'utilisation des méthodes formelles plus simples, en abaissant la barrière d'entrée pour être accessible à des non-experts, en apportant une meilleure IHM et des gains incrémentaux en termes de qualité et de réutilisation des composants logiciels », expliqueArnaud Charlet, responsable projets chez AdaCore.

Le projet Hi-Lite va aboutir à la création de deux nouveaux langages (SPARK 2014 et E-ACSL), d'outils (gnatprove, gnat2why, greffon Frama-C…), de bibliothèques, d'interfaces, etc.

Il s'agissait également de bénéficier du meilleur des deux mondes (preuve exhaustive d'absence d'erreurs d'exécution), ce que ne permet pas le test et de faciliter une utilisation mixte des tests unitaires et des preuves formelles à partir d'un langage commun. Deux nouveaux langages ont d'ailleurs été conçus: un langage de programmation étendu SPARK 2014 (disponible le premier trimestre 2014),basé surAda 2012, et E-ACSL qui repose sur les langagesACSL et C. « Le fait de disposer d'une sémantique et d'un langage communs donne une très grande valeur ajoutée, au niveau de l'aide à l'écriture et à la mise au point des contrats, d'inciter à l'utilisation de contrats logiciels, de ne pas dépendre d'une seule approche, de faciliter le passage de l'un à l'autre et vice-versa, etc.», ajoute Arnaud Charlet.

Accélérer les projets de grande taille

Autres résultats du projet, un ensemble d'outils a été développé. On trouve les traducteurs gnatprove et gnat2why, pour passer de SPARK 2014 au langage intermédiaireWhy et générer des résultats de preuve, ainsi que le greffon Frama-C (E-ACSL vers C en fournissant la sémantique exécutable du langage ACSL qui manquait jusque-là). D'autres outils ont été améliorés: GNAT Pro et GNATtest avec l'ajout de la sémantique exécutable du langage SPARK 2014, le prouveur Alt-Ergo, les plates-formes Why3 et Frama-C.Au-delà de la création d'outils et de bibliothèques, le projet Hi-Lite se traduira par une solution économique permettant aux industriels de réduire leurs coûts et le recours au test, d'accélérer le développement des projets de grande taille, de faciliter la certification des systèmes…