Praxis has won a contract with Thales UK to support its aircraft management software development.
Praxis will 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 software for evaluation and validation of mission plans, and to ensure that this software is developed to the required standard Spark Ada is being used as part of the development process.
Spark provides a programming language and verification environment for high-integrity software.
The core Spark language combines an unambiguous subset of the Ada programming language, 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.