Rockwell Collins Selects SPARK Pro for Security and Information Assurance
SPARK tools complement GNAT Pro for High Assurance Software projects
NEW YORK and SAN JOSE, Calif. – April 27, 2010 – Embedded Systems Conference – AdaCore, a leading supplier of Ada development tools and support services, today announced the selection of SPARK Pro by Rockwell Collins for use on selected projects that have stringent security and information assurance requirements. Rockwell Collins chose SPARK Pro for several reasons, including:
- previous SPARK development experience where the use of SPARK clearly reduced defects, shortened integration time, and aided certification,
- integrated SPARK toolset support provided in the GNATbench and GNAT Programming Studio (GPS) Interactive Development Environments (IDEs),
- SPARK support access using AdaCore’s “GNAT Tracker” system, including direct access to the SPARK developers and experts at Altran Praxis, and
- AdaCore’s customer friendly license and support subscription model.
SPARK Pro comprises the proven SPARK language toolset developed by Altran Praxis integrated into AdaCore’s GNAT Pro Ada development environment. The SPARK language supports the correctness-by-construction methodology (C-by-C) through which developers can create software and prove that it correctly implements system requirements. SPARK Pro is a natural solution for safety-critical and high-security programs, where failure could lead to catastrophic consequences.
A major factor in Rockwell Collins’ selection of SPARK Pro was their successful past experience both with the SPARK language and toolset from Altran Praxis and with AdaCore. Rockwell Collins has been using GNAT Pro on a number of projects, and they have found AdaCore’s support services, including the GNAT Tracker web interface, especially valuable. GNAT Tracker provides customers with on-line access to all products and associated documentation purchased, via a simple web interface. Engineers may report problems or ask questions; each report is automatically sent to the AdaCore product development team, ensuring fast and accurate responses. After submitting a report, the customer can use the associated ticket number to view questions and responses and to track the full history of the reported issue.
“Our subscription model encourages customers to contact us as often and frequently as they need,” said Robert Dewar, AdaCore President and CEO. “Our partnership with Altran Praxis allows us to extend this same service to SPARK Pro. SPARK Pro users, such as Rockwell Collins, will benefit from Altran Praxis’s experience with formal methods and the SPARK language, coupled with AdaCore’s support infrastructure, Ada language expertise and tool support.”
The SPARK toolset performs static (before run time) 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 to meet the requirements of industry regulators and certification schemes. SPARK checks for deep and subtle bugs, including run-time errors such as buffer overflow and arithmetic overflow, and can even verify that application-specific safety and security properties are not violated. The latest release of SPARK Pro, V9.0, includes a number of enhancements, including new information-flow verification for safety and security, a new tool that detects unreachable code, and a new SPARK 2005 language profile.
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 18,000 staff across the world. www.altran-praxis.com
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 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/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, railroad 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
Press Contacts
press@adacore.com