General Dynamics UK selects SPARK language for major new Royal Navy helicopter project

Praxis has today announced that General Dynamics UK has selected Praxis’ SPARK language as part of its £6 million contract to develop the safety-critical Stores Management System for the Royal Navy’s new AgustaWestland AW159 Lynx Wildcat helicopter.

SPARK is a high level programming language and toolset designed for writing software for high integrity applications. General Dynamics UK selected SPARK for the project owing to its ability to enable the development and verification of software to the highest level of Ministry of Defence safety certification – Defence Standard (Def Stan) 00-56 issue 2 Safety Integrity Level 4.

SPARK enables the application of formal verification techniques in a segregated monitor architecture, ensuring rapid compliance.

Up to seven developers will use SPARK to create the Stores Management System, which controls the deployment of weaponry from the AW159 Lynx Wildcat. Project development completes in mid 2011 and will cover more than 40,000 lines of SPARK code.

The AW159 Lynx Wildcat (formerly called the Future Lynx) will be the Royal Navy’s new maritime surveillance and attack helicopter. Scheduled to enter service in 2015, 28 helicopters have been ordered for the Royal Navy. The AW159 will provide ship defence against surface threats, act in an anti-submarine role and operate as a light utility helicopter.

The Stores Management System will enable the AW159 to operate the lightweight Sting Ray torpedo as well as the anticipated Future Air-to-Surface Guided Weapon (FASGW).

General Dynamics UK has used SPARK across its Stores Management System product line since the early 1990s. Previous projects include systems for the Tornado, Harrier and Typhoon aircraft.

"Meeting strict safety-critical certification is central to the new Stores Management System for the AW159 Wildcat," said Steve Hewitt, Programme Manager, Mission & Security Systems, General Dynamics UK Limited. "Our ongoing partnership with Praxis meant that SPARK was the natural choice when it came to developing this mission-critical application to the highest safety standards."

Developed by Praxis, SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. 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.

"General Dynamics UK is an extremely mature user of Praxis' SPARK technology, and I am delighted that they have once again chosen our technology for a new development project," said Keith Williams, Praxis Managing Director. "This secures SPARK as a core tool for assuring the integrity of advanced weapons systems with its use on a wide range of air platforms."