Presentation

Tool name

GNATprove

Website (if available)

http://www.open-do.org/projects/hi-lite/gnatprove/

Contact email

Hi-Lite mailing list: [email protected]

Main usage:

• Modelling [NO]
• Code generation [YES]
• Test case generation [NO]
• Model verification [NO]
• Code verification [YES]
• Test harness generation [YES]
• Other (Please elaborate)

Summary

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.

Publications

• 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 Verication 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.

Applicability

Key capabilities

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)

Two outputs:

• Native machine code
• Proof of code correctness with respect to the formal specification

Main restrictions

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).

Automated: proofs.

Expertise level

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

Yes.

Underlying technologies

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.

Traceability

No specific traceability facility.

Team work:

Tool relies on text code that can be easily shared like any source code source a Version Control System.

Certification issues:

Ada tools are used for developing SIL4 (or equivalent) safety critical software in railway, aeronautics, defence, ... domains.

Ada 2012 is an ISO standard.

Participants

AdaCore company.

Stable or recommended version of the tool

GNAT GPL Edition 2012.

Tool available for openETCS participants?

Yes.

If yes, Under which licence?

GNU GPL.

If no, or not under an Open Source licence, are there plan to do it?

Licenses of underlying technologies

Eclipse interface

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 / ...).

Planned development

All further developments that are relevant for openETCS, even if not conducted directly within the project.