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. »
Arnaud Charlet est responsable du projet Hi-Lite chez AdaCore.
