AdaCore, en association avec Altran Praxis, CEA-List, Astrium Space Transportation, INRIA-ProVal et Thales Communications, annonce le démarrage du projet Hi-Lite. Soutenu financièrement par le gouvernement français et le conseil général de l’Essonne, Hi-Lite est un projet Open Source conçu pour accroître l’utilisation des méthodes formelles dans le développement d’un logiciel hautement intégré, afin de répondre plus particulièrement au nouveau standard aéronautique DO-178C. Pour y parvenir, ce projet vise à développer des produits plus simples, plus puissants et plus faciles à utiliser.
Hi-Lite réunira les forces des partenaires du projet pour créer des outils de vérification formelle en langages Ada et C. La vérification du code pourra se faire à un niveau plus approfondi que les solutions actuelles et diminuer ainsi le recours à des tests physiques coûteux et consommateurs de temps des logiciels fortement intégrés. Le projet de 3,9 millions d’euros devrait durer trois ans.
Ce projet s’appuie sur l’expérience acquise pendant 10 ans sur l’utilisation des méthodes de vérification formelles par Airbus pour créer des systèmes de haute intégrité et est largement piloté par les critères générés par le travail d’Airbus : solidité, application au code, utilisation par des ingénieurs « lambda » sur des ordinateurs « standards », amélioration sur les méthodes classiques et possibilité de certification.
Ce projet est structuré autour de deux chaînes d’outils différents Ada et C. AdaCore sera le leader du projet et apportera son expertise dans le langage Ada, ainsi que le compilateur GNAT et l’analyseur statique CodePeer, tandis qu’Altran Praxis fournira son ensemble d’outils de vérification SPARK basé sur Ada. La chaîne d’outils C utilisera le compilateur GCC et la plate-forme Frama-C du CEA. Ces deux chaînes d’outils seront intégrées dans les IDE d’AdaCore.
Astrium Space Transportation démontrera la méthode et les outils en les déployant sur un gros projet pour redévelopper les systèmes logiciels de son véhicule de transfert automatisé visant à prouver les bénéfices de la vérification formelle. Thales Communications utilisera également les outils sur sa solution middleware basée sur un composant, ajoutant la capacité d’automatiser la vérification du code généré en utilisant le langage d’annotation Hi-Lite.
En définissant un langage commun d’annotations pour le test, l’analyse statique et les preuves formelles, Hi-Lite permettra à toutes les industries de passer graduellement d’une politique de test à tout va à des méthodes de vérification plus rapides et plus économiques. Il intègre de manière non-étroite des preuves formelles avec des tests et de l’analyse formelle, permettant ainsi de combiner différentes techniques dans les projets autour d’une expression commune de propriétés et de contraintes.
Le projet Hi-Lite est principalement géré par le supplément des méthodes formelles du standard aéronautique DO-178C. Pour la première fois, il permet aux outils de vérification formelle de remplacer les tests physiques au moment de la certification du système. Tout comme pour l’aéronautique et la défense, les produits créés au travers d’Hi-Lite ont pour objectif de rendre disponible la vérification formelle et de faciliter son utilisation dans de nombreuses industries comme le médical et l’automobile.
Pour obtenir de plus amples informations et de mises à jour régulières sur le projet Hi-Lite, visitez le site : http://open-do.org/projects/hi-lite
Citations des partenaires du projet Hi-Lite
« Les systèmes de haute intégrité étant de plus en plus complexes et intenses, les méthodes formelles représentent une solution économique qui diminue le recours aux tests et accélère la finalisation du projet », a déclaré Arnaud Charlet, responsable du projet Hi-Lite chez AdaCore. « Notre collaboration avec les partenaires du projet Hi-Lite a pour objectif d’accélérer et de faciliter la vérification formelle sur de nombreux gros projets multi-langage qui ont besoin de se conformer aux critères de certification comme le futur standard DO-178C ».
« Altran Praxis est ravi d’être impliqué dans le projet Hi-Lite. Nous pensons que le projet apportera des bénéfices à la vérification formelle et que l’approche SPARK atteindra un plus grand intérêt dans la communauté du développement logiciel », a déclaré Keith Williams, directeur d’Altran Praxis.
« CEA-LIST apportera son expertise sur la plate-forme Frama-C pour la preuve formelle du logiciel basé sur le langage C. Nous travaillerons sur la connexion des parties Ada et C des spécifications et des preuves », a déclaré Loïc Correnson, responsable de l’équipe Frama-C chez CEA-LIST. « Bien sûr, en tant que co-auteur du langage de spécification ACSL, nous participerons à l’élaboration du langage de spécification dans ce projet ».
« L’équipe ProVal du centre de recherche de l’INRIA à Saclay est heureuse de faire partie du projet Hi-Lite », a déclaré Claude Marché, chercheur en chef à l’INRIA. « Nous apporterons notre expertise dans le raisonnement hypothétique et dans les améliorations nécessaires à la chaîne d’outils de vérification déductive Why/Alt-Ergo.
A propos d’AdaCore
Fondée en 1994, AdaCore propose des solutions de développement logiciel pour Ada, un langage de programmation conçu spécifiquement pour répondre aux besoins des applications industrielles pour lesquelles la sûreté, la sécurité et la fiabilité sont essentielles. La gamme de produits d’AdaCore s’articule autour de son environnement de développement GNAT Pro, disponible sur de nombreuses plates-formes et du support qui l’accompagne. AdaCore dispose d’une large clientèle (voir à http://adacore.com/home/company/customers/ pour de plus amples information ).
Ada et GNAT Pro sont de plus en plus utilisés pour des applications critiques et certifiées, dans des secteurs tels que l’aéronautique, les systèmes militaires, la gestion/contrôle du trafic aérien, le transport ferroviaire ou encore les équipements médicaux, ainsi que les services financiers où la sécurité est déterminante.
Le siège social nord-américain d’AdaCore est à New York et le siège social européen est basé à Paris.
Site web : www.adacore.com
Contact presse :
Jamie Ayre
AdaCore
email : press@adacore.com
