Le projet Hi-Lite veut imposer la validation formelle pour les sytèmes critiques

AdaCore et ses partenaires Altran Praxis, CEA-List, Astrium Space Transportation, l'Inria-Proval et Thales Communications, ont annoncé hier le projet Hi-Lite, qui vise à créer des outils de vérification formelle en langages Ada et C. Ce projet, dont l'enveloppe globale a été fixée à 3,9 millions d'euros sur trois ans, est financé à hauteur de 1,4 millions d'euros par le gouvernement français et le conseil général de l'Essonne, dans le cadre du pôle de compétitivité System@tic Paris-Région.

Pour les applications logicielles complexes et critiques, comme les systèmes embarqués dans l'avionique ou l'aérospatiale par exemple, Hi-Lite veut répondre au besoin de vérification formelle du code. Estimant qu'« au niveau économique, on arrive à un pallier de blocage », le directeur général d'AdaCore, Cyrille Comar, explique que « les méthodes formelles ont du mal à s'installer dans l'industrie, alors qu'on développe des systèmes de plus en plus critiques. » Les méthodes actuelles, basées sur des tests industriels, ont la capacité de valider le fonctionnement de tous les paramètres d'un code, mais n'offrent pas de vérification formelle de l'ensemble du code et des scénarios qu'il peut mettre en oeuvre pour arriver à un but.

Les méthodes empiriques actuelles ne suffisent plus, et une demande forte pour de la vérification formelle existe. Le projet Hi-Lite veut donc lever un verrou technologique important. « Nous voyons des méthodes universitaires qui commencent à être fiables, nous devons maintenant fournir une passerelle clé-en-main vers l'industrie. »

Des entreprises comme Astrium, Thales Communications ou Airbus pourront donc être des utilisateurs finaux. Mais l'idée de Cyrille Comar n'est pas de s'arrêter là, et de proposer à terme une offre commerciale. D'autres secteurs que l'aéronautique et l'aérospatiale pourraient être intéressés : « on attend tous le moment où le problème avec les nouvelles voitures sera tel qu'il faudra être plus sérieux. Je ne dis pas que l'industrie n'est pas sérieuse, mais elle n'a pas encore pris la mesure du problème comme l'aéronautique, alors qu'il y a une explosion des logiciels embarqués. »

Plus de sécurité, une vérification qui pourra être validée par la future norme DO178C... Et une solution open-source, voici le cocktail que prévoit AdaCore pour les industriels dans le futur. Une conception chère à Cyrille Comar, qui explique qu'il croit « à des équipes relativement modestes : nous avons six partenaires seulement sur le projet, ce qui nous permet d'être très dynamiques. L'open-source est aussi important, car c'est une garantie de compétitivité. Nous sommes obligés d'apporter tout ce qui va autour du logiciel : notre expertise, notre garantie, et d'avoir toujours une longueur d'avance par rapport à une concurrence qui peut reprendre nos logiciels comme elle le souhaite. »