New consortium aims to promote formal methods for high integrity software

Financially supported by the French Government and the Essonne general council, Hi-Lite is aimed particularly at meeting the DO-178C avionics standard through the use of software tools that are simpler, more powerful and easier to use. The Hi-Lite team says it will bring together the project partners to create formal verification tools for both the Ada and C languages. These will, they say, 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, and builds on the existing 10 year experience of Airbus in using formal verification methods to create high integrity systems. Its goal is to carry on that work, predicated on Airbus' requirement that systems have to be robust, usable by 'normal' engineers on 'normal' computers, and improve on classical methods. Astrium says it 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 will also use the project tools across its middleware, adding the ability to automate verification of generated code by using the Hi-Lite annotation language.