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 »
Headlines
2012-02-03: We will present this paper on how to integrate formal program verification with testing at ERTS 2012 conference. Here is an example used in the paper to demo the techniques and tools.
Related Initiatives
The Workshop on Theorem Proving in Certification is now organized as a recurring event to compare approaches and tools based on theorem proving to critical software (such as avionics software), where a certification standard applies (DO-178B/C for avionics software). Here is the 2010 workshop and the 2011 workshop.
The tool ImProve performs formal verification (via model checking) on a small Embedded Domain Specific Language inside Haskell, and code generation to C.
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 »
Videos
Hi-Lite: a Verification Toolkit for Unit Test & Unit Proof
A presentation by Yannick Moy, Senior Engineer, AdaCore, at a recent talk at IRILL Days 2010. Video courtesy of IRILL (http://www.irill.org)
An Introduction to Open DO
A presentation by Cyrille Comar, Managing director of AdaCore Europe
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 news and events on Project Hi-Lite: Hi-Lite News and Events Page »
For the latest papers and presentations on Project Hi-Lite: Hi-Lite Resources 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