AdaCore and Altran Praxis Release SPARK Pro 10

SPARK Pro is a product jointly developed by Altran Praxis, international specialist in embedded and critical systems engineering, and AdaCore, the leading provider of commercial software solutions for the Ada language. SPARK Pro provides the foremost language, toolset and design discipline for engineering high-assurance software. It combines Altran Praxis’ acclaimed SPARK language and verification tools, with the GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments from AdaCore. There are SPARK versions based on Ada 83, Ada 95, and Ada 2005, so all standard Ada compilers and tools work out-of-the-box with SPARK.

SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness that can be used to meet the requirements of safety and security certification schemes such as DO-178B and the Common Criteria.

SPARK Pro 10’s new features include:

Automatic selection of flow analysis mode
The SPARK Pro Examiner now supports automatic selection of information flow or data flow analysis on a per-subprogram basis. This new feature increases flexibility for users by making it easier to analyse SPARK programs which have derives annotations (information flow contracts) only on certain subprograms, for example at the lower levels in the call tree or in those areas of the program with the highest integrity level requirements. This increased flexibility can equally be applied to facilitate the integration of SPARK code with non-SPARK or legacy code (e.g., full Ada or C). It also allows programs to be developed initially without derives annotations, and to have derives annotations added at a later stage as necessary.

KCG Language Profile
As part of a collaborative development with Esterel Technologies, a new language profile has been added to the Examiner for processing automatically-generated SPARK code produced by Esterel’s KCG code generator for SCADE. The SPARK/Ada version of KCG for SCADE will be available in Q4 of 2011 and further releases of both the SCADE and SPARK Pro toolsets in 2011 and 2012 will provide users with a route to static verification of automatically-generated SPARK code. The integration of these technologies will afford users the benefits of model-driven development with the assurance of a secure programming language and associated verification tool suite.

Derived Numeric Types
Definition of numeric types has been made easier by the introduction of language and tool support for explicitly derived numeric types. This removes the need for a user-supplied base type assertion and removes the risk of the user indicating a base type that is inconsistent with the target.

SPARKBridge preview for Windows
SPARKBridge – a bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers – was initially introduced as a GNU/Linux-only preview in SPARK Pro 9.1. SPARK Pro 10 extends this preview to Windows users, allowing them to experiment with alternate provers for discharging Verification Conditions. A fully-supported version of SPARKBridge will be available in future releases of the Black Belt edition of SPARK Pro.

Library Additions
The SPARK library has been augmented with several new packages including Interfaces, Ada.Characters.Handling, and Ada.Text_IO.

Proof Tools
A number of improvements have been made to the SPARK Pro proof tools. The Simplifier now has enhanced reasoning capabilities for modular types, allowing more proofs to be automatically discharged. In addition, the proof summary output (from the POGS tool) has been improved to make the management of the proof process easier for large projects.