Development & verification environment supports SPARK 2014

2nd May 2014

AdaCore

Staff Reporter

0 0

Offering an integrated approach to the entire software development and verification lifecycle, Altran and AdaCore have released SPARK Pro 14.0. The integrated development and verification environment provides users with more powerful and easier to use tools that support the latest version of the SPARK language, SPARK 2014. The product brings software specification, coding, testing and unit verification by proof within a single integrated framework.

SPARK Pro 14.0 has been completely re-engineered to use the latest compiler and proof technology, providing advanced verification of an enhanced subset of the Ada language. The new technology also supplies an improved user interface: warnings generated by the tools are displayed as navigable messages mapped back to the source code with path information that helps users understand how the errors can occur.

SPARK Pro 14.0 meets the requirements of all high-integrity software safety standards, including DO-178B/C (and the formal methods supplement DO-333), CENELEC 50128, IEC 61508, and DEFSTAN 00-56. The SPARK Pro toolset generates evidence that can be used to build a constructive assurance case and demonstrate conformance to the appropriate standard. SPARK Pro can also be used to help achieve the highest Evaluation Assurance Levels (EAL) of the Common Criteria security standard. Building software that is right the first time avoids the costs associated with extensive test and debug cycles and expensive product failures and recalls.

“Given the widespread use of Intelligent Systems across many sectors, the adoption of the new SPARK 2014 technology makes complete business sense” said Keith Williams, Group Vice President, Intelligent Systems / Altran. “Our clients need to ensure user requirements are met and costly events such as recalls are avoided ... SPARK Pro 14.0 does both”.

SPARK Pro 14.0 is the first version of the toolset to support SPARK 2014, the newest version of the language. SPARK 2014 is based on Ada 2012 and encompasses a rich subset of the language, excluding only those features which would make program verification unsound. SPARK uses and extends the contract notation introduced in Ada 2012, allowing software engineers to express and formally verify key properties that must be satisfied by a program.

“After decades as a niche technology, we have finally reached the stage where formal proof techniques can play an important part in the development of a wide range of software” said Robert Dewar, co-founder and President of AdaCore. “SPARK Pro 14.0 embodies the new promise of this technology.”

SPARK Pro 14.0 is available immediately.