LONDON General Dynamics U.K. has selected Praxis' SPARK language as part of its £6 million (about $10 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 U.K. is to use SPARK for the project as it can 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.
Developed by Praxis (Bath, England), 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.