L’éditeur franco-américain AdaCore, spécialisé dans les solutions logicielles pour le langage Ada, vient d’annoncer l’aboutissement du projet Hi-Lite auquel il participait avec Altran, Astrium Space Transportation, le CEA List, l'Inria Toccata et Thales Communications, et financé en partie par Oséo et le Conseil général de l'Essonne. Doté d’un budget de 3,9 millions d'euros sur trois ans, ce projet open source 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 tests deviennent une activité consommatrice de temps et de ressources, notamment lors de la conformité aux standards avioniques (norme DO-178B ou sa nouvelle version 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 coûts, de qualité et de réutilisation des composants logiciels », explique Arnaud Charlet, responsable de projets chez AdaCore. Autres résultats du projet, les premiers outils intégrant le test et la vérification formelle pour les programmes Ada et C ont été développés : le langage de programmation SPARK, via sa future version 2014, pour Ada et la plate-forme Frama-C pour C, ces deux technologies s'appuyant sur les outils de preuve de programmes développés par l'Inria.
5 juin 2013