Altran Praxis English language selection button
Altran Praxis French language selection button
Altran Praxis English language label
Altran Praxis Logo
Altran Praxis Technology image

SPARK

What is SPARK?

SPARK is a programming language and a set of software development products for high assurance software. The SPARK programming language is the only language specifically designed to support the development of safety or security critical software. In combination with the SPARK toolset, SPARK prevents, detects and eliminates defects early in the lifecycle as the source code is developed. It is, effectively, the result of applying the principles of Correctness by Construction to the design of a programming language and associated verification tools.

Why use SPARK?

It is important that software errors are eliminated at source. This is the fundamental principle of Correctness by Construction. At the level of the source code, this means using a programming language whose semantics are well-defined, and hence that will be amenable to error detection before execution of the software. SPARK – an annotated subset of Ada – is designed to do exactly that.

Based on decades of research into programming language design and verification technology by Altran Praxis, the SPARK Pro Toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. For example, the SPARK tools offer rigorous and automated proof of the absence of so-called “runtime errors” such as buffer overflow and divide-by-zero. Furthermore, the tools are designed to offer soundness for this analysis – they find all the defects, rather than just some subset of them.

The SPARK Pro tools are so efficient that they can be applied in a modular, constructive fashion during design – in line with the principles of Correctness by Construction and Lean Systems Thinking – thus preventing defects and confirming correctness as early as possible. Subsequent testing, rework and risk are therefore reduced. 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.

SPARK customers

  • Alenia AerMacchi
  • Alenia Difesa
  • Alstom Transport
  • Ansaldo STS
  • AWE
  • BAE Systems (Operations) Ltd.
  • BAE Systems Australia Ltd.
  • CESG
  • Data Systems and Solutions
  • EuroFighter Consortium
  • General Dynamics UK
  • Invensys Rail
  • Lockheed Martin
  • MBDA
  • QinetiQ
  • Rockwell Collins
  • Rolls-Royce Aero Engine Controls
  • Thales UK
  • Ultra Electronics

Want to learn more?

Details of SPARK Training, Support, the SPARK Textbook, Language Definition are available to view.

Availability

The SPARK Pro product-line is available world-wide through our partnership with AdaCore. For more information visit the SPARK Pro site.

Altran Praxis and AdaCore partnership logo

Customer support

Support for SPARK Pro is available through AdaCore’s GNAT Tracker infrastructure.

We also support long-term SPARK users.

Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc and is not based on the SPARC™ architecture.

Case reference

Lockheed Martin C-130J

Altran Praxis SPARK case image

Challenge

Lockheed Martin wanted to transform the Hercules’ avionics and other systems to create the Hercules II, or C-130J, air-lifter. The Operational Flight Programme (OFP) software coordinates and controls most of the avionics systems and operates and diagnoses the integrated aircraft. The integrity of the OFP software was under the intensive scrutiny of two of the world’s most stringent regulators: the US FAA and the UK MoD.

Engagement and approach

Praxis and Lockheed applied SPARK technology to the development and verification of the OFP software. The code was developed in SPARK and underwent analysis with the SPARK Examiner. This provided early visibility of programming errors which would have otherwise been detected much later in the testing phase, when correction costs would have been substantially greater.

Outcome

Praxis demonstrated that static analysis during implementation can lead to overall cost savings by reducing the amount of testing effort at later stages of the life-cycle. Given that DO-178B requires an extensive and rigorous testing process, this saving is often substantial and leads to much improved time to market.
"Very few errors have been found in the software during the most rigorous levels of FAA testing, which is being successfully conducted for less than a fifth of the normal cost in industry".
Jim Sutton, Lockheed Martin