Select Language

AdaCore Announces Successful Completion of Project Hi-Lite

Open Source project eases high integrity software development by combining formal methods with testing

PARIS and NEW YORK, May 29th 2013 – AdaCore and its research partners today announced the successful completion of Project Hi-Lite, a three-year, €3.9 million effort aimed at popularizing formal methods in the development of high integrity software by combining formal verification and testing. Hi-Lite took advantage of Airbus’ decade-long experience using formal verification methods to create high integrity systems, and leveraged the powerful industrial tools already developed by the project partners. The work was sponsored by the French Government and the General Council of the Département of Essonne and was conducted by a partnership comprising AdaCore, Altran, Astrium Space Transportation, CEA List, INRIA Toccata and Thales Communications.

Hi-Lite’s main goal was to make formal verification faster and easier to use across large, multi-language projects that need to meet safety certification criteria, and the project has successfully achieved this objective. “Hi-Lite has allowed us to take advanced program proving technology that was developed in academia and adapt it for industrial use,” said Yannick Moy, Hi-Lite Project Manager at AdaCore. “The project has shown that formal verification can complement testing and play a prominent and practical role in verifying critical software.”

Testing is often time consuming and costly, especially when the software has to comply with standards such as DO-178B or its recent revision DO-178C for commercial airborne systems (used by certification authorities including the FAA, EASA and Transport Canada). As high integrity systems grow in size and complexity, formal methods like those investigated in the Hi-Lite project provide a cost-effective solution that decreases the need for testing, speeds up project development, and facilitates system certification. These techniques are especially relevant in a DO-178C context, in light of the Formal Methods Supplement (DO-333) that provides standard guidance on how formal analysis fits into the verification process.

The HI-Lite project has produced the first tools that can integrate testing and formal verification for both Ada and C programs - the SPARK toolset for Ada and the Frama-C platform for C. Both toolchains rely on state-of-the-art program proving tools developed by Project Hi-Lite partner INRIA. Theoretical and practical advances resulting from the project, and from these tools, have been published in more than thirty international conferences and journals, including Embedded World and IEEE Software. The usability of the project’s tools and methodology has been documented in published industrial case studies from Hi-Lite partners Astrium Space Transportation and Altran. All the tools developed are Open Source, and prototype versions are available at https://forge.open-do.org/projects/hi-lite/ and http://frama-c.com.

As an immediate benefit of Project Hi-Lite, the methodologies developed there are being used by AdaCore and its partner Altran to shape the upcoming revision to the SPARK language, known as SPARK 2014. SPARK, an Ada subset augmented with annotations that formalize various program properties, is a high integrity language with a proven track record in software at the highest levels of safety and security. SPARK is the only modern imperative programming language designed with sound static verification as its primary goal. It is supported by the SPARK Pro toolset that combines Altran’s SPARK language and verification tools with AdaCore’s GNAT Programming Studio (GPS) development environment. SPARK Pro prevents, detects and eliminates defects early in the life-cycle as the source code is developed. The technologies developed in Project Hi-Lite will be fully integrated into the SPARK Pro toolset to make it SPARK 2014-compliant. More information on the SPARK 2014 release can be found at http://www.spark-2014.org.

About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the open source GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see http://www.adacore.com/home/company/customers/ for further information.

Ada and GNAT Pro see a growing usage in high integrity and safety-certified applications, including space-based systems, commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains, such as financial services. The SPARK Pro toolset, available from AdaCore, is especially useful in such contexts.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com

Press Contacts
Jamie Ayre
AdaCore
press@adacore.com
http://twitter.com/AdaCoreCompany

Jessie Glockner
Rainier Communications (for AdaCore)
Tel: 508-475-0025 x140
adacore@rainierco.com
http://twitter.com/JessieGlockner

AdaCore annonce la réussite du projet Hi-Lite.

Ce projet Open Source facilite le développement de logiciels critiques en associant méthodes formelles et tests.

PARIS et NEW YORK 29 mai 2013 - AdaCore et ses partenaires ont annoncé aujourd'hui la réussite du Projet Hi-Lite, un projet au budget de 3,9 millions d'euros qui s'est étendu sur trois ans. L'objectif du projet était de démocratiser les méthodes formelles dans le développement de logiciels critiques en associant la vérification formelle et le test. Le projet Hi-Lite s'est appuyé sur l'expérience acquise pendant dix ans par Airbus pour créer des systèmes critiques en utilisant des méthodes de vérification formelles et sur les outils industriels performants déjà développés par les partenaires du projet. Les travaux ont été financés en partie par le gouvernement français et le Conseil Général de l'Essonne et ont été réalisés en partenariat par AdaCore, Altran, Astrium Space Transportation, CEA List, INRIA Toccata et Thales Communications.

L'objectif principal de Hi-Lite était de rendre la vérification formelle plus rapide et facilite d'utilisation pour les projets de grande taille impliquant plusieurs langages de programmation, et soumis à des critères de certification. Le projet a rempli cet objectif. "Hi-Lite nous a permis d'adapter des technologies de pointe développées dans les Universités à une utilisation industrielle", a déclaré Yannick Moy, responsable du projet Hi-Lite chez AdaCore. "Le projet a montré que la vérification formelle peut remplacer ou compléter les activités de test et jouer un rôle prédominant dans la vérification des logiciels critiques".

Le test est une activité consommatrice de temps et de ressources, notamment lorsque le logiciel doit se conformer aux standards tels que le DO-178B ou sa nouvelle version DO-178C pour les systèmes avioniques civils (qui sont utilisés par les organismes de certification comme le FAA, EASA et Transport Canada). Alors que les systèmes critiques continuent à croître en taille et en complexité, les méthodes formelles comme celles qui ont été utilisées dans le projet Hi-Lite apportent une solution économique faisant diminuer le recours au test, accélérer le développement de projets et faciliter la certification des systèmes. Ces techniques sont spécialement pertinentes dans un environnement DO-178C, à la lumière du supplément pour les méthodes formelles (DO-333) qui apporte des indications sur la façon dont l'analyse formelle s'intègre dans le processus de vérification.

Le projet Hi-Lite a produit les premiers outils intégrant le test et la vérification formelle pour les programmes Ada et C. Il s'agit des outils SPARK pour Ada et de la plate-forme Frama-C pour C. Ces deux technologies s'appuient sur les outils de preuve de programmes développés par l'INRIA, partenaire du projet Hi-Lite. Les avancées pratiques et théoriques résultant de ce projet et de ces outils ont été publiées dans plus de trente conférences et journaux internationaux, parmi lesquels Embedded World et IEEE Software. L'utilisation des outils et de la méthodologie du projet a été expliquée et publiée sous forme d'études de cas par les partenaires Astrium Space Transportation et Altran. Tous les outils développés sont Open Source et les prototypes sont disponibles sur : https://forge.open-do.org/projects/hi-lite/ et http://frama-c.com.

Une conséquence immédiate du projet Hi-Lite est que les méthodologies développées sont actuellement utilisées par AdaCore et son partenaire Altran pour façonner la nouvelle version du langage SPARK, connue sous le nom de SPARK 2014. SPARK, un sous-ensemble d'Ada complété par des annotations qui formalisent différentes propriétés des programmes, est un langage de programmation reconnu pour faciliter la création de logiciels devant atteindre les plus hauts niveaux de sûreté et de sécurité. SPARK est le seul langage de programmation moderne conçu avec comme premier objectif une vérification statique sûre. L'utilisation du langage SPARK est liée à la boîte à outils SPARK Pro, composée du langage et des outils de vérification SPARK d'Altran et de l'environnement de développement GNAT Programming Studio (GPS) d'AdaCore. SPARK Pro permet de prévenir, détecter et éliminer les défauts très tôt dans le cycle de vie du projet, lors du développement du code source. Les technologies développées dans le projet Hi-Lite seront entièrement intégrées dans les outils SPARK Pro pour les rendre conformes à SPARK 2014. Plus d'informations sur la disponibilité prochaine de la version SPARK 2014 à l'adresse : http://www.spark-2014.org.

À propos d’AdaCore

AdaCore, fondé en 1994, est le premier fournisseur de solutions logicielles commerciales pour Ada, un langage de programmation de pointe conçu pour des applications de grande taille et à grande durée de vie. Les technologies fournies par AdaCore sont particulièrement adaptées aux applications pour lesquelles la sûreté, la sécurité et la fiabilité sont des éléments critiques.  Le produit phare d'AdaCore est l'environnement de développement GNAT Pro, disponible sur le plus vaste ensemble de plateformes de toutes les technologies Ada. Il est fournit avec un support en ligne dispensé par des experts parmi les plus reconnus dans le domaine.  AdaCore dispose d’une large base de clients située dans le monde entier ; voir http://www.adacore.com/home/company/customers/ pour de plus amples informations.

L'utilisation d'Ada et de GNAT Pro connaît une croissance continue dans les applications critiques ou certifiées pour la sûreté, comme les éléments d'avionique pour les appareils commerciaux, les systèmes militaires, le contrôle aérien, les systèmes ferroviaires, les appareils médicaux, et dans des domaines sensibles pour la sécurité comme les services financiers.

Le siège social d’AdaCore est situé à Paris pour la zone Europe, et à New York pour la zone Amérique du Nord. http://www.adacore.com

Contacts Presse

Jamie Ayre
AdaCore
press@adacore.com
http://twitter.com/AdaCoreCompany