NEW YORK and PARIS, June 7, 2011 – 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/
About Altran Praxis
Altran Praxis is a specialist systems and software house, focussed on the engineering of systems with demanding safety, security or innovation requirements. Altran Praxis leads the world in specific areas of advanced systems engineering and innovation such as: ultra low defect software engineering, Human Machine Interface (HMI), safety engineering for complex or novel systems, systems engineering and methods/tools (such as SPARK). Altran Praxis offers clients a range of services including turnkey systems development, consultancy, training and R&D. Key market sectors are aerospace and defence, rail, nuclear, air traffic management, automotive, medical and security. The company operates globally with active projects in the US, Asia and Europe. The headquarters of Altran Praxis are in Bath (UK) with offices in Sophia Antipolis, London, Paris, Loughborough and Bangalore.
Altran Praxis is an expertise centre within the Altran Group (altran.com) – a global leader in innovation engineering, employing over 17,000 staff across the world. www.altran-praxis.com
About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore’s flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see http://www.adacore.com/home/company/customers/ for further information.
Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including commercial aircraft avionics, military systems, air traffic management/control, railway systems and medical devices, and in security-sensitive domains such as financial services.
AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com
