Initié en 2010, doté d'une enveloppe globale de 3,9 millions d’euros et financé à hauteur de 1,4 million par les pouvoirs publics dans le cadre du pôle de compétitivité Systematic, le projet de recherche industrielle Hi-Lite trouve aujourd’hui son épilogue. Porté par la société Adacore, fournisseur d’outils de développement et de test pour le langage Ada, ce projet s'est attaché à évaluer comment l’utilisation des méthodes de preuve formelle pouvait améliorer les méthodes de test des codes embarqués critiques. ...

Basées sur la mise en œuvre d’une description mathématique d’un programme, les techniques de preuve formelle ont deux intérêts principaux. D’une part, elles assurent (au sens fort du terme) qu’il n’y a pas d’erreurs dans un programme et, d’autre part, elles peuvent être facilement automatisées. Revers de la médaille, ces méthodes sont difficiles à maîtriser et réclament une expertise très forte de la part des ingénieurs qui les manipulent. Pourtant, il existe une demande réelle de la part des développeurs de logiciels embarqués d’avoir à disposition des outils génériques et aisément manipulables par les ingénieurs de test "normaux". C'est le cas chez Airbus qui utilise déjà depuis une dizaine d’années des approches à base de preuve formelle. En arrière-plan, se tapit aussi une problématique économique, car les opérations de test de codes embarqués critiques, de plus en plus complexes et soumis à des contraintes de certification, explosent littéralement. Il s’agit donc de trouver des voies pour diminuer les coûts du test en automatisant une partie d’entre eux, tout en conservant un très haut niveau de fiabilité et de confiance dans les résultats obtenus.

Le projet Hi-Litea mené des travaux en ce sens. Outre Adacore, le projet a réunit la société d’ingénierie Altran, les sociétés Astrium Space Transportation et Thales Communications et les laboratoires CEA-List et Inria. Pour Yannick Moy, responsable du projet Hi-Lite chez Adacore, « l’adaptation des technologies de preuves formelles développées au sein des universités a été réalisée en vue d'une mise en œuvre résolument industrielle, et le projet a clairement montré que la vérification formelle peut être un complément très efficace des stratégies de test des logiciels critiques, voire même remplacer certaines d’entre elles. »

Deux langages

Après avoir compilé un certain nombre d’exigences lors de la première année du projet, les travaux ont ensuite porté sur le développement d’outils, de bibliothèques et d’interfaces utilisateurs qui permettent aux technologies de preuve formelle d’être intégrées dans un environnement de développement classique et d'être utilisées par un ingénieur, sans modification de son univers traditionnel de travail. Avec, à la clé, la définition de deux langages accompagnés de leurs manuels de référence respectifs : le Spark 2014, basé sur la version 2012 du langage Ada, et le E-ACSL, basé sur les langages ACSL (ANSI C Specification Language) et le C. Ces deux langages, pour la première fois, pourront à la fois être utilisés pour les preuves formelles et pour les tests statiques classiques, grâce à une sémantique commune pour les deux types d’opérations. Ils permettront notamment d’inciter les programmeurs à utiliser des annotations au sein du code, et donc favoriseront une approche de programmation par contrat (introduite en particulier il y a quelques années dans le langage Eiffel), avec pour la première fois la possibilité d’exécuter ces contrats.

    L'un des résultats importants du projet Hi-Lite est de pouvoir mixer, au sein d'un seul environnement de développement classique, la mise en oeuvre de tests statiques et la vérification par la preuve formelle, et ce grâce à l'ajout, dans le programme, d'annotations spécifiques (qui sont vérifiées mathématiquement).   Spark 2014, qui va être industrialisé par Adacore et Altran, sera définitivement disponible au premier trimestre de l’année prochaine. Selon Adacore, il y a d’ores et déjà une communauté active de quelques 300 utilisateurs Spark dans le monde et une dizaine d’universités l’enseigne.   Quand au langage E-ACSL, et ce n’est pas la moindre des avancées du projet Hi-Lite, il est intégré au sein du framework Frama-C, issu du CEA-List. Car, si Ada est un langage écrit nativement pour supporter des contraintes en termes de fiabilité, il n’en est pas de même pour le C. Or ce dernier est évidemment très utilisé dans un nombre incalculable de systèmes embarqués, même les plus critiques. Rappelons que Frama-C est né en 2005 d’une volonté commune du CEA-List et de l’Inria de fusionner leurs efforts de développement pour proposer un outil open source capable « d’utiliser des techniques d'analyse plus variées et d'autoriser leur combinaison pour contourner les faiblesses de chacune, de vérifier des logiciels non forcément issus de systèmes embarqués critiques, et d’ouvrir la plate-forme de façon à permettre à quiconque de développer ses propres analyseurs », explique Julien Signoles, ingénieur de recherche au CEA-List. D’ailleurs, des analyseurs non issus du CEA-List et développés par des industriels comme Airbus, Atos Origin, Dassault Aviation, Adelard, Safe River ou TrustMySoft (une toute jeune société issue du CEA qui qui va se concentrer sur la sécurité logicielle) sont opérationnels et utilisés au sein du framework Frama-C. « L'outil est en cours de qualification pour pouvoir être utilisé dans un programme avionique chez Airbus soumis à la DO-178C », précise Julien Signoles. A la suite du projet Hi-Lite, la sémantique exécutable du E-ACSL a été définie, un traducteur des annotatoons E-ACSL vers le C pour la vérification des assertions à l'exécution a été écrit, et la plate-forme Frama-C a évolué pour en améliorer l’usage.