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, has kicked off in France.
Called Hi-Lite, it will 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," said project member AdaCore.
The €3.9 million project is scheduled to last three years and is supported financially the French government and the Essonne general council.
Alongside AdaCore are Altran Praxis, CEA LIST, Astrium Space Transportation, INRIA ProVal and Thales Communications.
Hi-Lite builds on ten years of experience at Airbus in using formal verification methods to create high integrity systems.
"It 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," said AdaCore.
There will be 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 tool chain will use the GCC compiler and CEA's Frama-C platform.
Both tool chains will be integrated within AdaCore's development environment.
Astrium Space Transportation will demonstrate the method and tools by deploying them on a 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," said AdaCore. "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."
Hi-Lite 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," said AdaCore. "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."