Réduire les cycles de développement des logiciels complexes.
DR

L’éditeur français AdaCore, en association avec Altran Praxis, le CEA-List, Astrium Space Transportation, l'INRIA-ProVal et Thales Communications, annonce le démarrage de Hi-Lite. Ce projet Open Source vise à accroître l'utilisation des méthodes formelles dans le développement des logiciels 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.

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

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 qu’avec 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, soutenu financièrement par L’Etat et le Conseil Général de l'Essonne, 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 "standard" ; amélioration sur les méthodes classiques et possibilité de certification.

Deux chaînes d’outils Ada et C

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 environnements de développement intégrés (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.

Réduire les tests physiques

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.

Jean-François Prevéraud

Pour en savoir plus : http://open-do.org

x

Email de votre ami :

Votre Nom :

Votre Email :

Saisissez le code de sécurité *