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, 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.
Alenia Aermacchi, Alenia Difesa, Alstom Transport, Ansaldo STS, AWE, BAE Systems (Operations) Ltd., BAE Systems Australia Ltd., CESG, Data Systems and Solutions, Invensys Rail, EuroFighter Consortium, General Dynamics UK, Lockheed Martin, MBDA, QinetiQ, Rockwell Collins, Rolls-Royce Aero Engine Controls, Thales UK, Ultra Electronics.
Want to learn more?
More information about SPARK, including answers, videos and webinars, can be found here.
For information about training, please see the course descriptions and course schedule here.
The SPARK Pro product-line is available world-wide through our partnership with AdaCore. Please go to the AdaCore SPARK Pro site for more details.
Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc and is not based on the SPARC™ architecture.
Lockheed Martin C-130J
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
Altran 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.
Altran 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.