{"id":2913,"date":"2010-05-06T10:56:50","date_gmt":"2010-05-06T10:56:50","guid":{"rendered":"http:\/\/www.agglotv.com\/?p=2913"},"modified":"2010-05-06T10:56:50","modified_gmt":"2010-05-06T10:56:50","slug":"adacore-presente-le-projet-hi-lite-nouveau-consortium-visant-a-promouvoir-les-methodes-formelles-pour-un-logiciel-fortement-integre","status":"publish","type":"post","link":"https:\/\/www.agglotv.com\/?p=2913","title":{"rendered":"AdaCore pr\u00e9sente le projet Hi-Lite : Nouveau consortium visant \u00e0 promouvoir les m\u00e9thodes formelles pour un logiciel fortement int\u00e9gr\u00e9"},"content":{"rendered":"<div class=\"alignleft\"><script type=\"text\/javascript\"><!--\ngoogle_ad_client = \"pub-2913804460579993\";\n\/* 250x250, date de cr\u00e9ation 28\/04\/10 *\/\ngoogle_ad_slot = \"1337509044\";\ngoogle_ad_width = 250;\ngoogle_ad_height = 250;\n\/\/-->\n<\/script><br \/>\n<script type=\"text\/javascript\"\nsrc=\"http:\/\/pagead2.googlesyndication.com\/pagead\/show_ads.js\">\n<\/script><\/div>\n<p><strong>AdaCore, en <a href=\"http:\/\/www.association-gael.org\">association<\/a> avec Altran Praxis, CEA-List, Astrium Space Transportation, INRIA-ProVal et Thales Communications, annonce le d\u00e9marrage du projet Hi-Lite. Soutenu financi\u00e8rement par le gouvernement fran\u00e7ais et le conseil g\u00e9n\u00e9ral de l&rsquo;<a href=\"http:\/\/www.rest-hotels.com\/essonne-c-62.html\">Essonne<\/a>, Hi-Lite est un projet Open Source con\u00e7u pour accro\u00eetre l&rsquo;utilisation des m\u00e9thodes formelles dans le d\u00e9veloppement d&rsquo;un logiciel hautement int\u00e9gr\u00e9, afin de r\u00e9pondre plus particuli\u00e8rement au nouveau standard a\u00e9ronautique DO-178C. Pour y parvenir, ce projet vise \u00e0 d\u00e9velopper des produits plus simples, plus puissants et plus faciles \u00e0 utiliser.<\/strong><\/p>\n<p>Hi-Lite r\u00e9unira les forces des partenaires du projet pour cr\u00e9er des outils de v\u00e9rification formelle en langages Ada et C. La v\u00e9rification du code pourra se faire \u00e0 un niveau plus approfondi que les solutions actuelles et diminuer ainsi le recours \u00e0 des <a href=\"http:\/\/www.domicilgym.fr\/boutique\/14-materiel-de-test\">tests physiques<\/a> co\u00fbteux et consommateurs de temps des logiciels fortement int\u00e9gr\u00e9s. Le projet de 3,9 millions d&rsquo;euros devrait durer trois ans.<\/p>\n<p>Ce projet s&rsquo;appuie sur l&rsquo;exp\u00e9rience acquise pendant 10 ans sur l&rsquo;utilisation des m\u00e9thodes de v\u00e9rification formelles par Airbus pour cr\u00e9er des syst\u00e8mes de haute int\u00e9grit\u00e9 et est largement pilot\u00e9 par les crit\u00e8res g\u00e9n\u00e9r\u00e9s par le travail d&rsquo;Airbus : solidit\u00e9, application au code, utilisation par des ing\u00e9nieurs \u00ab\u00a0lambda\u00a0\u00bb sur des ordinateurs \u00ab\u00a0standards\u00a0\u00bb, am\u00e9lioration sur les m\u00e9thodes classiques et possibilit\u00e9 de certification.<!--more--><\/p>\n<p>Ce projet est structur\u00e9 autour de deux cha\u00eenes d&rsquo;outils diff\u00e9rents Ada et C. AdaCore sera le leader du projet et apportera son expertise dans le langage Ada, ainsi que le compilateur GNAT et l&rsquo;analyseur statique CodePeer, tandis qu&rsquo;Altran Praxis fournira son ensemble d&rsquo;outils de v\u00e9rification SPARK bas\u00e9 sur Ada. La cha\u00eene d&rsquo;outils C utilisera le compilateur GCC et la plate-forme Frama-C du CEA. Ces deux cha\u00eenes d&rsquo;outils seront int\u00e9gr\u00e9es dans les IDE d&rsquo;AdaCore.<\/p>\n<p>Astrium Space Transportation d\u00e9montrera la m\u00e9thode et les outils en les d\u00e9ployant sur un gros projet pour red\u00e9velopper les syst\u00e8mes logiciels de son v\u00e9hicule de transfert automatis\u00e9 visant \u00e0 prouver les b\u00e9n\u00e9fices de la v\u00e9rification formelle. Thales Communications utilisera \u00e9galement les outils sur sa solution middleware bas\u00e9e sur un composant, ajoutant la capacit\u00e9 d&rsquo;automatiser la v\u00e9rification du code g\u00e9n\u00e9r\u00e9 en utilisant le langage d&rsquo;annotation Hi-Lite.<\/p>\n<p>En d\u00e9finissant un langage commun d&rsquo;annotations pour le test, l&rsquo;analyse statique et les preuves formelles, Hi-Lite permettra \u00e0 toutes les industries de passer graduellement d&rsquo;une politique de test \u00e0 tout va \u00e0 des m\u00e9thodes de v\u00e9rification plus rapides et plus \u00e9conomiques. Il int\u00e8gre de mani\u00e8re non-\u00e9troite des preuves formelles avec des tests et de l&rsquo;analyse formelle, permettant ainsi de combiner diff\u00e9rentes techniques dans les projets autour d&rsquo;une expression commune de propri\u00e9t\u00e9s et de contraintes.<\/p>\n<p>Le projet Hi-Lite est principalement g\u00e9r\u00e9 par le suppl\u00e9ment des m\u00e9thodes formelles du standard a\u00e9ronautique DO-178C. Pour la premi\u00e8re fois, il permet aux outils de v\u00e9rification formelle de remplacer les tests physiques au moment de la certification du syst\u00e8me. Tout comme pour l&rsquo;a\u00e9ronautique et la d\u00e9fense, les produits cr\u00e9\u00e9s au travers d&rsquo;Hi-Lite ont pour objectif de rendre disponible la v\u00e9rification formelle et de faciliter son  utilisation dans de nombreuses industries comme le m\u00e9dical et l&rsquo;automobile.<\/p>\n<p>Pour obtenir de plus amples informations et de mises \u00e0 jour r\u00e9guli\u00e8res sur le projet Hi-Lite, visitez le site : <a href=\"http:\/\/open-do.org\/projects\/hi-lite\">http:\/\/open-do.org\/projects\/hi-lite<\/a> <\/p>\n<p><strong>Citations des partenaires du projet Hi-Lite<\/strong><\/p>\n<p>\u00ab\u00a0Les syst\u00e8mes de haute int\u00e9grit\u00e9 \u00e9tant de plus en plus complexes et intenses, les m\u00e9thodes formelles repr\u00e9sentent une solution \u00e9conomique qui diminue le recours aux tests et acc\u00e9l\u00e8re la finalisation du projet\u00a0\u00bb, a d\u00e9clar\u00e9 Arnaud Charlet, responsable du projet Hi-Lite chez AdaCore. \u00ab\u00a0Notre collaboration avec les partenaires du projet Hi-Lite a pour objectif d&rsquo;acc\u00e9l\u00e9rer et de faciliter la v\u00e9rification formelle sur de nombreux gros projets multi-langage qui ont besoin de se conformer aux crit\u00e8res de certification comme le futur standard DO-178C\u00a0\u00bb.<\/p>\n<p>\u00ab\u00a0Altran Praxis est ravi d&rsquo;\u00eatre impliqu\u00e9 dans le projet Hi-Lite. Nous pensons que le projet apportera des b\u00e9n\u00e9fices \u00e0 la v\u00e9rification formelle et que l&rsquo;approche SPARK atteindra un plus grand int\u00e9r\u00eat dans la communaut\u00e9 du d\u00e9veloppement logiciel\u00a0\u00bb, a d\u00e9clar\u00e9 Keith Williams, directeur d&rsquo;Altran Praxis.<\/p>\n<p>\u00ab\u00a0CEA-LIST apportera son expertise sur la plate-forme Frama-C pour la preuve formelle du logiciel bas\u00e9 sur le langage C. Nous travaillerons sur la connexion des parties Ada et C des sp\u00e9cifications et des preuves\u00a0\u00bb, a d\u00e9clar\u00e9 Lo\u00efc Correnson, responsable de l&rsquo;\u00e9quipe Frama-C chez CEA-LIST. \u00ab\u00a0Bien s\u00fbr, en tant que co-auteur du langage de sp\u00e9cification ACSL, nous participerons \u00e0 l&rsquo;\u00e9laboration du langage de sp\u00e9cification dans ce projet\u00a0\u00bb.<\/p>\n<p>\u00ab\u00a0L&rsquo;\u00e9quipe ProVal du centre de recherche de l&rsquo;INRIA \u00e0 Saclay est heureuse de faire partie du projet Hi-Lite\u00a0\u00bb, a d\u00e9clar\u00e9 Claude March\u00e9, chercheur en chef \u00e0 l&rsquo;INRIA. \u00ab\u00a0Nous apporterons notre expertise dans le raisonnement hypoth\u00e9tique et dans les am\u00e9liorations n\u00e9cessaires \u00e0 la cha\u00eene d&rsquo;outils de v\u00e9rification d\u00e9ductive Why\/Alt-Ergo.<\/p>\n<p><strong>A propos d&rsquo;AdaCore <\/strong><br \/>\nFond\u00e9e en 1994, AdaCore propose des solutions de d\u00e9veloppement logiciel pour Ada, un langage de programmation con\u00e7u sp\u00e9cifiquement pour r\u00e9pondre aux besoins des applications industrielles pour lesquelles la s\u00fbret\u00e9, la s\u00e9curit\u00e9 et la fiabilit\u00e9 sont essentielles. La gamme de produits d\u2019AdaCore s\u2019articule autour de son environnement de d\u00e9veloppement GNAT Pro, disponible sur de nombreuses plates-formes et du support qui l\u2019accompagne. AdaCore dispose d&rsquo;une large client\u00e8le (voir \u00e0 <a href=\"http:\/\/adacore.com\/home\/company\/customers\/\">http:\/\/adacore.com\/home\/company\/customers\/<\/a> pour de plus amples information ).<\/p>\n<p>Ada et GNAT Pro sont de plus en plus utilis\u00e9s pour des applications critiques et certifi\u00e9es, dans des secteurs tels que l\u2019a\u00e9ronautique, les syst\u00e8mes militaires, la gestion\/contr\u00f4le du trafic a\u00e9rien, le transport ferroviaire ou encore les \u00e9quipements m\u00e9dicaux, ainsi que les services financiers o\u00f9 la s\u00e9curit\u00e9 est d\u00e9terminante.<br \/>\nLe si\u00e8ge social nord-am\u00e9ricain d&rsquo;AdaCore est \u00e0 New York et le si\u00e8ge social europ\u00e9en est bas\u00e9 \u00e0 <a href=\"http:\/\/www.rest-hotels.com\/paris-c-64.html\">Paris<\/a>.<br \/>\nSite web : <a href=\"http:\/\/www.adacore.com\">www.adacore.com<\/a> <\/p>\n<p><strong>Contact presse :<\/strong><br \/>\nJamie Ayre<br \/>\nAdaCore<br \/>\nemail : press@adacore.com <\/p>\n","protected":false},"excerpt":{"rendered":"<p>AdaCore, en association avec Altran Praxis, CEA-List, Astrium Space Transportation, INRIA-ProVal et Thales Communications, annonce le d\u00e9marrage du projet Hi-Lite. Soutenu financi\u00e8rement par le gouvernement fran\u00e7ais et le conseil g\u00e9n\u00e9ral de l&rsquo;Essonne, Hi-Lite est un projet Open Source con\u00e7u pour accro\u00eetre l&rsquo;utilisation des m\u00e9thodes formelles dans le d\u00e9veloppement d&rsquo;un logiciel hautement int\u00e9gr\u00e9, afin de r\u00e9pondre [&hellip;]<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":[],"categories":[5],"tags":[],"amp_enabled":true,"_links":{"self":[{"href":"https:\/\/www.agglotv.com\/index.php?rest_route=\/wp\/v2\/posts\/2913"}],"collection":[{"href":"https:\/\/www.agglotv.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.agglotv.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.agglotv.com\/index.php?rest_route=\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.agglotv.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=2913"}],"version-history":[{"count":1,"href":"https:\/\/www.agglotv.com\/index.php?rest_route=\/wp\/v2\/posts\/2913\/revisions"}],"predecessor-version":[{"id":2914,"href":"https:\/\/www.agglotv.com\/index.php?rest_route=\/wp\/v2\/posts\/2913\/revisions\/2914"}],"wp:attachment":[{"href":"https:\/\/www.agglotv.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=2913"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.agglotv.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=2913"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.agglotv.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=2913"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}