A Technical Overview of SPARK

The SPARK Language

SPARK exploits the strengths of Ada while eliminating all its potential ambiguities and insecurities. A SPARK program has a precise meaning which is unaffected by the choice of Ada compiler and can never be erroneous. These desirable goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted tasking) and partly by introducing annotations or "formal comments" to capture the code designer's intentions. The combination of these approaches allows SPARK-in both its '83 and '95 variants-to meet its design objectives which are: rigorous definition, simple semantics, security, expressive power, verifiability and bounded resource requirements.


The SPARK Examiner

The Examiner is a free-standing software tool that assists programming in SPARK from the design stage onwards. The Examiner-itself written in SPARK-operates, like a compiler, directly on source files. Errors and warnings are reported where they occur in listing files. SPARK programs can be compiled by any Ada compiler. SPARK supports the progressive refinement of a program design towards its final implementation. The Examiner can check the coherence of the text at every stage, even of skeletal designs and partial implementations before compilation is possible. In this way error detection is brought forward and correctness by construction achieved.

The Examiner performs two kinds of static analysis. The first, made up of language conformance checks and flow analysis, checks that the program is "well-formed" and is consistent with the design information included in its annotations. This stage is extremely straightforward and can be readily incorporated into the coding phase of the development process. After these checks the source is known to be free from erroneous behaviour and free from conditional and unconditional data flow errors (i.e. use of uninitialised data) on a system-wide basis (including abstract state in package bodies).

The second, optional, kind of analysis is verification: showing by proof that the SPARK program has certain specified properties. The most straightforward is a proof that the code is exception free; this adds Constraint_Error to the list of possible errors eliminated by SPARK. Proof can also be used to demonstrate, unequivocally, that the code maintains important safety or security properties or even to show its complete conformance with some suitable specification.


SPARK Benefits

The advantages of precision of expression and early error detection are enormous. It is well known that the cost of error correction rises rapidly if errors are not detected until late in the development cycle; precisely where they are found if testing is the only verification strategy employed. By eliminating whole classes of possible error and facilitating the early discovery of those that remain, SPARK reduces cost and risk. One large avionics project used a mix of programming languages and was subject to a rigorous independent verification process; this showed that SPARK code-which had been subjected only to the first well-formation stage of analysis-had only one tenth of the residual anomalies as comparable full Ada and only one hundredth of those found in parts of the system written in C.

When used throughout the development process, SPARK can also have a beneficial effect on designs. Consideration of information flows at the design stage leads to programs with the desirable properties of abstraction, encapsulation, high cohesion and loose coupling. The complementary INFORMED design method exploits SPARK's properties to meet these goals.

SPARK is also consistent with the requirements of all important standards and is at the heart of the technical report ISO/IEC DTR 15942 "Guide for the Use of the Ada Programming Language in High Integrity Systems". For systems developed to RTCA DO-178B SPARK brings significant technical and cost benefits. Correctness by construction means that the expensive formal test process required by the standard is not wastefully used as a means of error detection and does not generate rework. The savings here are very significant: one avionics project completed Level A formal testing for less than one fifth of the normal cost in industry. The high test coverage requirements of the standard are also simplified if Ada's run-time checks are suppressed; SPARK's ability to prove the code to be exception free is a necessary foundation for taking this step. Finally, SPARK programs make significantly less use of the Ada run-time system than full Ada programs; this makes them highly-compatible with certifiable run-time kernels and removes another potential obstacle to Level A certification.

SPARK is also highly relevant to standards, such as UK Def Stan 00-55 and those based on IEC 6 1508, which require application of a range of validation techniques and the construction of a safety case. The ability to reason about the code, in the context of its system environment, to track and separate safety variables and to prove safety properties is central to the philosophy of these standards. For Def Stan 00-55, SPARK is the proven, low-risk solution. The UK MoD's flagship Def Stan 00-55 demonstrator project (SHOLIS) was coded entirely in SPARK, proved against its formal specification and has been faultless in acceptance and trials.

Where the objective is security rather than safety, SPARK is equally applicable and has a proven record in the production of systems up to ITSEC E6.


Training and Support

Effective use of SPARK is facilitated by the high quality of its documentation, training and support. The documentation is backed by the availability of the text book "High Integrity Software – The SPARK Approach" by the highly respected author John Barnes.

Courses on the use of SPARK, tailored to clients' particular requirements, can be provided either on their own sites or in Bath.

Under a standard maintenance agreement, SPARK users gain easy access to Praxis High Integrity Systems' team of skilled SPARK and Ada specialists who offer timely and comprehensive advice on the effective use of SPARK. Further advice on all aspects of high-integrity software development, including the management and execution of SPARK projects, can be provided by Praxis High Integrity Systems' world-class team of consulting engineers.