Project Hi-Lite has ended!
To download the SPARK Hi-Lite GPL 2013 release, go tolibre.adacore.com/tools/spark-gpl-edition/
frama-c.com/download.html
www.spark-2014.org
frama-c.com
Final project reports
- Final report on experimentations on industrial case studies
- Final report on evolutions in Why and Alt-Ergo (in French)
Slides presented during the final project meeting on May 29th, 2013
- Official presentation of project results (in French)
- EADS Astrium case studies results
- Frama-C developments related to E-ACSL
- Test and proof with E-ACSL in Frama-C
- Roadmap and challenges for SPARK 2014 and GNATprove
- Progress made in Alt-Ergo
Presentation
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 »
Related Initiatives
The OpenETCS project aims at integrating modeling, development, validation and testing in a common framework around open-source tools. See the GNATprove description at ETCS github repository.
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, 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 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
To get (read) access to the git repository, look at 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