AdaCore announces Hi-Lite project

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 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 defence, the products created through Hi-Lite aim to make formal verification available and easier to use across more industries such as medical and automotive.