Completion of Project Hi-Lite to improve verification for high integrity systems
NewsMay 30, 2013
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 high integrity systems that must comply with DO-178B/C. Hi-Lite techniques were developed in the context of the DO-333 Formal Methods Supplement that provides guidance on integrating formal analysis into the verification process, making them especially applicable for DO-178C 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, AdaCore. “The project has shown that formal verification 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 Ada 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 open source 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.
