General Dynamics has selected SPARK, a computer programming language developed by the critical systems engineering company Praxis, for use on the safety-critical stores management system aboard the UK Royal Navy’s new AW159 Lynx Wildcat helicopter.

SPARK is a high-level programming language and toolset intended to be secure and to support the development of safety and security applications.

The programming language enables the application of formal verification techniques in a segregated monitor architecture to ensure rapid compliance.

The stores management system controls the deployment of weaponry from the navy’s new maritime surveillance and attack helicopter, the AgustaWestland AW159 Lynx Wildcat, scheduled to enter service in 2015.

A total of seven developers will use SPARK to write more than 40,000 lines of code for the project which is expected to be complete in mid 2011.

General Dynamics UK contracted Praxis for SPARK as part of a £6m contract with the Royal Navy.