Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Website (if available)
Hi-Lite mailing list: email@example.com
- Modelling [NO]
- Code generation [YES]
- Test case generation [NO]
- Model verification [NO]
- Code verification [YES]
- Test harness generation [YES]
- Other (Please elaborate)
Part of the Hi-Lite project, GNATprove is a formal verification tool for Ada, based on the GNAT compiler. It can prove that subprograms respect their contracts, expressed as preconditions and postconditions in the syntax of Ada 2012. The tool automatically discovers the subset of subprograms which can be formally analyzed. GNATprove is currently available for x86 linux, x86 windows and x86-64 linux.
The GNATprove tool can be combined with regular testing tools to cover the whole program using the most efficient approaches.
- Hi-Lite: The Convergence of Compiler Technology and Program Verification http://www.open-do.org/wp-content/uploads/2012/11/HILT_2012.pdf
- Integrating Formal Program Verication with Testing http://www.open-do.org/wp-content/uploads/2011/12/hi-lite-erts2012.pdf
Support and Survivability
Commercial support through AdaCore company.
Tool is open-source (GPL license) and available at Hi-Lite project forge.
Regarding support, a mailing list is available.
The tool is supported by AdaCore, provider of GNAT Ada compilers since 1994.
Integration of proof and tests in the same framework using the same contract language, standardized in Ada 2012.
Input (which languages are targeted?)
Subset of Ada 2012 language (ISO standard) suitable for safety critical embedded software (no exception, no dynamic memory allocation, no pointer).
Output (Proof, code, other)
- Native machine code
- Proof of code correctness with respect to the formal specification
Only a subset of Ada (see above).
Manual or automated use of the tool
Manual: (1) code and (2) annotations on code (pre and post-conditions, loop invariants).
Middle level: training needed to write program contracts and loop invariants. But once this is done proof is done automatically.
Integration in the tool chain and development process
Currently distributed: Yes/No
GNAT development environment. An Eclipse integration is available for GNAT compiler (not yet for GNATprove).
GNATprove is currently available for x86 linux, x86 windows and x86-64 linux.
No specific traceability facility.
Tool relies on text code that can be easily shared like any source code source a Version Control System.
Ada tools are used for developing SIL4 (or equivalent) safety critical software in railway, aeronautics, defence, ... domains.
Ada 2012 is an ISO standard.
Stable or recommended version of the tool
GNAT GPL Edition 2012.
Tool available for openETCS participants?
If yes, Under which licence?
If no, or not under an Open Source licence, are there plan to do it?
Licenses of underlying technologies
Yes for GNAT compiler. Not yet for GNATprove.
Other integration possibilities
Existing industrial usage
Not used yet in industrial setting. A similar tool called SPARK and also maintained by AdaCore has been used in several industrial use cases.
List of projects or toolboxes (only list the representative examples) where the tool has been integrated + some information on the toolchain architecture that has been used (e.g. Eclipse Modelling / OSGi / UML / ...).
All further developments that are relevant for openETCS, even if not conducted directly within the project.