Using the SPARK Toolset for Showing the Absence of Run-Time Errors in Safety-Critical Software

  • Darren Foulger
  • Steve King
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2043)


This paper reports the results of a study into the effectiveness of the SPARK toolset for showing the absence of run-time errors in safety-critical Ada software. In particular, the toolset is examined to determine how effective it is in finding run-time errors in a SPARK program, and how much of the process of proving freedom from run-time errors can be performed automatically. The study identifies areas where automatic run-time checks are not so effective and, where possible, gives recommendations about the design of the software so that the toolset is as effective as possible in automatically proving absence of run-time errors.

The results will be of interest to anyone contemplating the use of the SPARK toolset for ensuring the absence of run-time errors, both as guidance in planning the effort required, and for practical advice on making the best use of the toolset.


Proof Checker Real Arithmetic Manual Proof Good Design Practice Real Number Arithmetic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. Barnes. High integrity Ada: The SPARK approach. Addison-Wesley, 1997.Google Scholar
  2. 2.
    D.M. Foulger. Evaluation of the SPARK toolset in checking for run-time errors in safety-critical software. MSc report, University of York, Heslington, York, UK, 2000.Google Scholar
  3. 3.
    D.M. Foulger. Results of study into run-time checks of SPARK programs. Technical Report BAe-BSY-RP-GEN-000008, Issue 1, BAE SYSTEMS, Brough, E. Yorkshire, July 2000.Google Scholar
  4. 4.
    MOD. The procurement of safety related software in defence equipment. UK Ministry of Defence, August 1997. DEF STAN 00-55 (Part 1: Requirements and Part 2: Guidance).Google Scholar
  5. 5.
    K.A. Nyberg, editor. The annotated Ada Reference Manual. ANSI, 1983. ANSI/MIL-STD-1815A-1983.Google Scholar
  6. 6.
    M. Saaltink and S. Michell. Ada95 trustworthiness study: guidance on the use of Ada95 in the development of high integrity systems. Technical Report TR-97-5499-04a, Version 2.0, Department of National Defence, Ottawa, Canada, March 1997.Google Scholar
  7. 7.
    SPARK — The SPADE Ada Kernel. Praxis Critical Systems, August 1997. Edition 3.3.Google Scholar
  8. 8.
    J.P. Thornley. Static analysis and diversity in the software development process — experiences with the use of SPARK. In K. Hardy and J. Briggs, editors, Reliable software technologies — Ada-Europe’ 97, number 1251 in Lecture Notes in Computer Science, pages 266–277. Springer-Verlag, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Darren Foulger
    • 1
  • Steve King
    • 2
  1. 1.BAE SYSTEMSBroughUK
  2. 2.Department of Computer ScienceUniversity of YorkHeslingtonUK

Personalised recommendations