/> SPARK Pro was created one year ago 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’ renowned SPARK language and verification tools, with the GNAT Programming Studio (GPS) and GNATbench development environments from AdaCore.

The new release of SPARK Pro 9 demonstrates the forward momentum of the toolset and introduces significant new features to benefit developers. Chief amongst these is the ability to mix software of different security levels (such as classified and unclassified) within the same system. This MILS functionality meets the increasing trend in the aerospace and defence industries to combine multiple secure and non-secure elements into a single system to deliver smaller, more integrated solutions.

“We’ve seen significant growth in the use of SPARK Pro since its launch last year across the safety critical and high assurance markets,” said Keith Williams, Altran Praxis Managing Director. “SPARK Pro 9 continues this market momentum and introduces important new features, particularly in the growing high security sector. It demonstrates the continuing benefits of our close partnership with AdaCore to our customers across the globe.”

Over half of new features in SPARK Pro 9 are the result of customer feedback. As well as support for the advanced features of SPARK2005, the latest version of the SPARK language, closer integration between SPARK and GPS results in improved usability and faster development times.

“In MILS-oriented Operating Systems, mixing safely different levels of security assurance requires a complex multi-partition organization. SPARK Pro 9 now provides the means to verify accurately such a mix in the context of a single application through sound information flow analysis,” said Cyrille Comar, Managing Director, AdaCore. “This capability offers an unprecedented level of flexibility for those writing rich applications with stringent security requirements.”

Developed by Praxis, SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital for reasons of safety, security, or both. The SPARK toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes. There are versions of SPARK 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 9 new functions include:

* New information-flow verification for safety and security policies, such as Bell-LaPadula, based on integrity labelling of variables, inputs and outputs. This facility allows users to confirm intended separation properties, and to prevent violations of the chosen information flow policy.
* SPARK2005. The new SPARK2005 language profile is now available. At present, Ada2005 features supported include ‘Mod, ‘Machine_Rounding, new reserved words, and the static semantics of “overriding.”
* New ZombieScope tool, which detects dead statements, branches and paths in SPARK code, complementing the capabilities of the Simplifier and proof status summarizer POGS.
* Cross Referencing annotations in GPS. The Examiner now generates cross-reference information that can be consumed by GPS to drive navigation within annotations.
* Function return annotations are now treated more like procedure post-conditions, being substituted into the VC hypotheses of the caller. This can dramatically improve the effectiveness of the theorem prover for those calling units, as well as reducing the manual work required by the user to provide rewrite rules.
* New output format for POGS. This format is designed to be both easier to read and easier to search automatically. It also reflects the results of the new ZombieScope tool.
* Simpler documentation structure. All proof material is now in one manual, and a new global index (in both clickable PDF and HTML forms) simplifies finding topics in the entire manual set.
* Case checking. New Examiner switch that insists on consistent casing within annotations.