AdaCore Announces Successful Completion of Project Hi-Lite

. Hi-Lite took advantage of Airbus’ decade-long experience using formal verification methods to create high integrity systems, and leveraged the powerful industrial tools already developed by the project partners. The work was sponsored by the French Government and the General Council of the Département of Essonne and was conducted by a partnership comprising AdaCore, Altran, Astrium Space Transportation, CEA List, INRIA Toccata and Thales Communications.

Hi-Lite’s main goal was to make formal verification faster and easier to use across large, multi-language projects that need to meet safety certification criteria, and the project has successfully achieved this objective. “Hi-Lite has allowed us to take advanced program-proving technology that was developed in academia and adapt it for industrial use,” said Yannick Moy, Hi-Lite Project Manager at AdaCore. “The project has shown that formal verification can complement testing and play a prominent and practical role in verifying critical software.”

Testing is often time consuming and costly, especially when the software has to comply with standards such as DO-178B or its recent revision DO-178C for commercial airborne systems (used by certification authorities including the FAA, EASA and Transport Canada). As high integrity systems grow in size and complexity, formal methods like those investigated in the Hi-Lite project provide a cost-effective solution that decreases the need for testing, speeds up project development, and facilitates system certification. These techniques are especially relevant in a DO-178C context, in light of the Formal Methods Supplement (DO-333) that provides standard guidance on how formal analysis fits into the verification process.

The Hi-Lite project has produced the first tools that can integrate testing and formal verification for both Ada and C programs - the SPARK toolset for Ada and the Frama-C platform for C. Both toolchains rely on state-of-the-art program-proving tools developed by Project Hi-Lite partner INRIA. Theoretical and practical advances resulting from the project, and from these tools, have been published in more than thirty international conferences and journals, including Embedded World and IEEE Software. The usability of the project’s tools and methodology has been documented in published industrial case studies from Hi-Lite partners Astrium Space Transportation and Altran. All the tools developed are Open Source, and prototype versions are available at https://forge.open-do.org/projects/hi-lite/ and http://frama-c.com.

As an immediate benefit of Project Hi-Lite, the methodologies developed there are being used by AdaCore and its partner Altran to shape the upcoming revision to the SPARK language, known as SPARK 2014. SPARK, an Ada subset augmented with annotations that formalise various program properties, is a high integrity language with a proven track record in software at the highest levels of safety and security. SPARK is the only modern imperative programming language designed with sound static verification as its primary goal. It is supported by the SPARK Pro toolset that combines Altran’s SPARK language and verification tools with AdaCore’s GNAT Programming Studio (GPS) development environment. SPARK Pro prevents, detects and eliminates defects early in the life-cycle as the source code is developed. The technologies developed in Project Hi-Lite will be fully integrated into the SPARK Pro toolset to make it SPARK 2014-compliant. More information on the SPARK 2014 release can be found at http://www.spark-2014.org.