Hi-Lite is a project aiming at popularizing formal methods for the development of high-integrity software. It targets ease of adoption through a loose integration of formal proofs with testing and static analysis, that allows combining techniques around a common expression of specifications. Its technical focus is on modularity, that allows a divide-and-conquer approach to large software systems, as well as an early adoption by all programmers in the software life cycle.
Hi-Lite is completely based on libre software. The project is structured in two different toolchains for Ada and C based on GNAT/GCC compilers, the SPARK verification toolset and the Frama-C platform. The integration of these toolchains inside two industrial IDEs offers to the user a common interaction on Ada and C programs. In particular, mixed Ada/C programs can be verified against a common specification.
Project Hi-Lite has officially launched and we will be reporting on its progress here as it reaches major milestones throughout the evolution of the project.
To get started on Hi-Lite, see
- a high-level view of the research context of Hi-Lite (in French, but see anyway the diagrams on slides 3 and 23)
- a description of the industrial context of Hi-Lite
- the initial technical project description (in French)
A "Lighter" Introduction to Hi-Lite
Hi-Lite is based on powerful industrial tools that have been developed by the different partners for the last 10 to 25 years. In order to show you how Hi-Lite can improve on the existing state-of-the-art by creating new communications between these tools, we describe in the following the application of the various tools and techniques that are part of Hi-Lite to a very simple program.
For the full story: Click here »
Funding
Hi-Lite is an Open Source project financially supported by the French Government and the Essone general council in an effort to increase the use of formal methods in developing high-integrity software, particularly to meet the forthcoming DO-178C avionics standard.
Partners
The project partners are AdaCore, Altran Praxis, Astrium Space Transportation, CEA-LIST, the ProVal team of INRIA and Thales Communications. AdaCore is the project leader.
For more information on partners: Hi-Lite Partners Page »
Video: Introducing Project Hi-Lite
You can also view the presentation slides if you want to follow along. Note that the Hi-Lite slides start on page 30..
More Resources
For the latest papers and presentations on Project Hi-Lite: Hi-Lite Resource Page »
To watch recent progress made in Project Hi-Lite: Hi-Lite Progress Page »
Get Involved
If you are interested in participating in the Hi-Lite effort: Open-DO Forge »
To participate in the technical discussions, subscribe to Hi-Lite mailing-list »
Contact
For more information about project Hi-Lite: info@open-do.org