Le projet



Porteur :
Appel à projet :
Statut :
Groupes Thématiques :
Date de début du projet :
Date de fin de projet :
Durée :
36 mois
Montant total :
3 900 K€
Montant aide :
1 409 K€
Axe :
Software engineering
Description :

• Hi-Lite's goal is to promote the use of formal methods in developing high-integrity software. It loosely integrates formal proofs with testing and static analysis, thus allowing projects to combine different techniques around a common expression of properties and constraints.

Hi-Lite's focus on modularity allows scaling to large software systems and
encourages early adoption. By relying only on sound static analyses, Hi-Lite
qualifies for being a tool of choice for industrial users needing to apply the
Formal Methods Supplement of the upcoming DO-178C standard.

Hi-Lite is completely based on free software. The project is structured as two
different tool-chains for Ada and C based on GNAT/GCC compilers (Ada and C), the
CodePeer static analyzer (Ada), the SPARK verification tool-set (Ada) and the
Frama-C platform (C), all integrated inside AdaCore IDEs.

Les données

Publication :
• Hi-Lite will create a set of workflows for critical software verification based on tools. It is expected that various products will be defined andcommercialized based on these workflows by the owners of the base tools: AdaCore, Altran, CEA and INRIA. In particular, the next version of the SPARK technology will be based directly on the results of the Hi-Lite project. The large scale experiments performed by industrial partners Altran, Astrium and Thales will give them a strong advance in the application of these workflows in their industrial context.