Altran and AdaCore have released an enhanced upgrade to their integrated development and verification environment for the ADA-based SPARK language, Version 14.0.
According to Keith Williams, Group Vice President, Intelligent Systems, at Altran, SPARK Pro 14.0 . represents a major step forward in software verification technology, providing users with more powerful and easier to use tools that support the latest version of the SPARK language, SPARK 2014.
SPARK Pro is the result of a partnership between AdaCore and Altran that was announced in 2009. It is an integrated static analysis toolsuite for developing and verifying high-integrity software and supports the SPARK 2014 language and provides advanced verification tools that are tightly integrated into the GNAT Programming Studio (GPS) IDE.
According to Robert Dewar, co-founder and President of AdaCore, 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,” he said.
It 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,” said Deewar. “It can also be used to help achieve the highest Evaluation Assurance Levels (EAL) of the Common Criteria security standard.”
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.
It 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 Dewar.
Using SPARK Pro, developers can formally define and automatically verify software architectural properties and functional requirements. This automated verification is particularly well-suited to applications where software failure is unacceptable.