SPARK Ada for Thales aircraft software system
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 is said to have 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 claims a combination of soundness, completeness,efficiency and analytical depth which is said to be unmatched by any other language. SPARK also is reported to meet all known regulatory requirements and standards for high- integrity software.
