Les Méthodes Formelles Se Démocratisent Grâce Au Projet Hi-lite

Le 01/10/2013 à 17:00  

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.

La lecture de cet article est payante.
Pour le lire abonnez-vous ou connectez vous.

Dans la même rubrique

Copy link
Powered by Social Snap