Altran and AdaCore Release Next-Generation Static Verification Toolset
SPARK Pro 14.0 brings new proof technology and additional language features to developers of high-integrity software
Altran and AdaCore announce the release of the SPARK Pro 14.0 integrated development and verification environment. This product marks 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 14.0 offers an integrated approach to the entire software development and verification lifecycle – bringing 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”.
Screen shot of SPARK Pro 14.0 in GNAT Programming Studio (GPS)
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.”
Pricing and availability
SPARK Pro 14.0 is available immediately. Further product information – including a demonstration – will be found on www.adacore.com/sparkpro. For more information about pricing and supported platforms please contact info@adacore.com.
About SPARK Pro
SPARK Pro is the result of a partnership between AdaCore and Altran that was announced in 2009. SPARK Pro is an integrated static analysis toolsuite for developing and verifying high-integrity software. It supports the SPARK 2014 language and provides advanced verification tools that are tightly integrated into the GNAT Programming Studio (GPS) IDE. 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.
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 open source 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/customers/for further information.
Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including space-based systems, commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains, such as financial services. The SPARK Pro toolset, available from AdaCore, is especially useful in such contexts.
AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com
About Altran
As global leader in innovation and high‐tech engineering consulting, Altran accompanies its clients in the creation and development of their new products and services. Altran's Innovation Makers have been providing services for thirty years to key players in the Aerospace, Automotive, Energy, Railways, Finance, Healthcare and Telecoms sectors. Covering every stage of project development from strategic planning to manufacturing, Altran’s offers capitalise on the Group’s technological know-how in five key areas: Intelligent Systems, Innovative Product Development, Lifecycle Experience, Mechanical Engineering, and Information Systems.
In 2013, the Group generated revenues of €1,633m. Altran now has a staff of over 21,000 employees in more than 20 countries.
www.altran.com
Press Contacts
Jamie Ayre
AdaCore
press@adacore.com
http://twitter.com/AdaCoreCompany
Owen Burdekin
Altran UK
+44 (0) 20 3117 0714
owen.burdekin@altran.com
Léonore Cousin
Altran group
+ 33 (0)1 46 41 72 10
press@altran.com
Follow us on Twitter #altranPR
Visit Altran’s new hub press