Completion of Project Hi-Lite to improve verification for high integrity systems

PARIS and NEW YORK. AdaCore has announced the completion of Project Hi-Lite, a joint research project focused on enhancing formal verification for multi-language, open-source software projects that require safety certification. Leveraging Airbus verification methods and industry tools, Project Hi-Lite combined formal proofs with testing and static analysis to improve the development of high integrity software. In the process, the Hi-Lite project also produced the first tools capable of integrating testing and formal verification for Ada and C programs.

The formal methods developed in Project Hi-Lite were targeted at reducing testing and facilitating certification, particularly for systems that must comply with /C. Hi-Lite techniques were developed in the context of the Formal Methods Supplement that provides guidance on integrating formal into the verification process, making them especially applicable for systems.

“Hi-Lite has allowed us to take advanced program proving technology that was developed in academia and adapt it for industrial use,” says Yannick Moy, Hi-Lite Project Manager, . “The project has shown that can complement testing and play a prominent and practical role in verifying critical software.”

Project Hi-Lite also resulted in the creation of tools capable of integrating testing and formal verification in and C languages. The SPARK toolset and Frama-C platform for the Ada and C languages, respectively, are based on tools developed by Project Hi-Lite partner INRIA. Prototype versions of the tools are available at https://forge.open-do.org/projects/hi-lite/and http://frama-c.com.

Partners in the Hi-Lite project include AdaCore, Altran, Astrium Space Transportation, CEA-LIST, the ProVal team of INRIA and Thales Communications. More information on Hi-Lite and other open source “DO” projects can be found at http://www.open-do.org.