Praxis wins contract to supply SPARK Ada for Thales aircraft software system

Praxis has won a contract with Thales UK, Air Operations in Wells, to supply the SPARK Ada toolset as part of ongoing product development by Thales in Aircraft Mission management and Mission Planning. Thales UK specialises in developing high integrity software for evaluation and validation of mission plans and to ensure that this software is developed to the required standard, SPARK Ada is used as part of a rigorous development process. One of the primary goals was to select a tool with a proven reputation in the Safety community. The SPARK tool met all of the requirements and is now being used on a major programme.

SPARK provides a programming language and verification environment for high-integrity software. The core SPARK language combines an unambiguous subset of Ada with annotations or "contracts" that allow wholly static verification of key program properties such as information-flow, absence of run-time errors, program correctness, and invariant safety and security properties. The toolset offers a combination of soundness, completeness, efficiency and analytical depth which is unmatched by any other language. SPARK also meets all known regulatory requirements and standards for high-integrity software.

"We are very pleased that Thales UK has selected SPARK for this programme" said Rod Chapman, SPARK Products Manager and Principal Engineer at Praxis. "This win further re-enforces SPARK's position as the de-facto choice for software where high-integrity or ultra-low defect rates are required."