AMSTERDAM, NY and PARIS--(Marketwire - March 24, 2010) - Avionics Europe 2010 -- SPARK Pro 9, announced today by AdaCore and Altran Praxis, provides a major step forward for developers creating safety critical and high assurance systems. The advanced open source development environment now features increased security functionality, including the ability to verify and assure Multiple Independent Levels of Security (MILS) within the same application as well as support for the latest SPARK2005 language profile.
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.
Webinar
A webinar providing an introduction and demonstration of SPARK Pro 9 will be held on April 27, 2010. It will begin at 5pm European Daylight Time/4pm GMT Daylight Time/11am Eastern Daylight Time/8am Pacific Daylight Time. To register please visit: http://www.adacore.com/home/products/gnatpro/webinars/
Availability
SPARK Pro 9 is available now. For more information please visit www.adacore.com or contact sales@adacore.com.
About Altran Praxis
Altran Praxis is a specialist systems and software house, focused 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 and tools (such as SPARK) /methods for systems engineering. It 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, and wholly owned by, Altran which is a global leader in innovation engineering and employs 17,000 staff across the world.
About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, the 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 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
Contact Information:
Press Contacts
Jamie Ayre
AdaCore
press@adacore.com
Jessie Glockner
Rainier Communications (for AdaCore)
Tel: 508 475 0025 x140
adacore@rainierco.com
Leena Chauhan
Altran Praxis
press@altran-praxis.com
Tel: +44 (0) 203 1170884
Chris Measures/Richard Morgan
Speed
altranpraxis@speedcommunications.com
Tel: +44 (0) 20 7842 3200