AdaCore Announces Hi-Lite Project

New consortium aims to promote formal methods for high integrity software

PARIS and NEW YORK, May 4, 2010 – AdaCore, together with Altran Praxis, CEA LIST, Astrium Space Transportation, INRIA ProVal and Thales Communications today announced the start of the Hi-Lite project. Financially supported by French national and local government agencies, Hi-Lite is an Open Source project designed to increase the use of formal methods in developing high integrity software, particularly to meet the forthcoming DO-178C avionics standard. It will achieve this by building tools that are simpler, more powerful and easier to use.

Hi-Lite will bring together the strengths of the project partners to create formal verification tools for both the Ada and C languages. These will enable code verification at a deeper level than current solutions and reduce the need for time-consuming and costly physical testing of high integrity software solutions. The €3.9 million ($5.3 million) project is scheduled to last three years.

The project builds on the existing ten year experience of Airbus in using formal verification methods to create high integrity systems, and is strongly driven by the criteria that Airbus’s work has generated: soundness, applicability to the code, usability by “normal” engineers on “normal” computers, improvement on classical methods, and certifiability.

The project is structured as two different tool chains for Ada and C. AdaCore will lead the project and contribute its expertise in the Ada language, including the GNAT compiler and CodePeer static analyser, with Altran Praxis providing its Ada-based SPARK verification toolset. The C toolchain will use the GCC compiler and CEA’s Frama-C platform. Both toolchains will be integrated within AdaCore’s IDEs.

Astrium Space Transportation will demonstrate the method and tools by deploying them on a major project to redevelop the software systems of its Automated Transfer Vehicle, aiming to prove the advantages of formal verification. Thales Communications will also use the project tools across its component-based middleware solution, adding the ability to automate the verification of generated code by using Hi-Lite annotation language.

By defining a common language of annotation for testing, static analysis and formal proofs, Hi-Lite will allow industries to switch gradually from an all testing policy to a faster and more cost-effective use of verification methods. It loosely integrates formal proofs with testing and static analysis, thus allowing projects to combine different techniques around a common expression of properties and constraints.

The Hi-Lite project is primarily driven by the planned Formal Methods Technology Supplement of the DO-178C avionics standard. For the first time, this allows formal verification tools to replace physical testing when applying for system certification. As well as aerospace and defense, the products created through Hi-Lite aim to make formal verification available and easier to use across more industries, such as medical and automotive.

For more information and regular updates on the Hi-Lite project visit http://www.open-do.org/projects/hi-lite

Quotes from the Hi-Lite project partners

“As high integrity systems get larger and more complex, formal methods provide a cost-effective solution that decreases the need for testing and speeds up project completion,” said Arnaud Charlet, Hi-Lite Project Leader of AdaCore. “Working with the Hi-Lite project partners, we aim to make formal verification faster and easier to use across large, multi-language projects that need to meet certification criteria, such as the forthcoming DO-178C standard.”

“Altran Praxis are delighted to be involved in Hi-Lite. We look forward to the project bringing the advantages of formal verification and the SPARK approach to a wider audience in the software development community,” said Keith Williams, Altran Praxis Managing Director.

“CEA-LIST will provide its expertise on the Frama-C platform for the formal proof of C-based software. We will work on connecting the Ada and C parts of the specifications and proofs,” said Loïc Correnson, leader of the Frama-C team at CEA-LIST. “Indeed, as a co-author of the ACSL specification language, we will participate in the elaboration of the specification language(s) in the project.”

“The ProVal Team at the INRIA Saclay research center is pleased to be a member of the Hi-Lite project,” said Claude Marché, Senior Research Scientist at INRIA. “We will provide expertise in automated reasoning and needed improvements in the Why/Alt-Ergo deductive verification tool-chain.”

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 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 commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains such as financial services.

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