Rockwell Collins Selects SPARK Pro for Security and Information Assurance

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.

Rockwell Collins selected SPARK Pro for the GPS modernisation project for several reasons; a major factor 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.