Hi-Lite; projet Open Source

AdaCore, en association avec Altran Praxis, CEA-List, Astrium Space Transportation, INRIA-ProVal et Thales Communications, a annoncé 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. Il 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.