AdaCore and Altran Praxis today announced the release of the SPARK Pro 10 software development and verification environment, providing a major step forward for the developers of high-assurance systems. SPARK Pro now offers increased flexibility to developers of systems with mixed integrity levels or with the need to integrate SPARK with other languages or legacy code.

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.

Availability
SPARK
Pro 10 is available now. For more information please visit http://www.adacore.com/home/products/sparkpro/ or contact info@adacore.com.

Webinar
A webinar providing an introduction to the new features in SPARK Pro 10 will be presented on the 5th July. For more information and to register please visit www.adacore.com/home/products/sparkpro/language_toolsuite/webinars/