Using the SPARK Toolset for Showing the Absence of Run-Time Errors in Safety-Critical Software
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.
KeywordsProof Checker Real Arithmetic Manual Proof Good Design Practice Real Number Arithmetic
Unable to display preview. Download preview PDF.
- 1.J. Barnes. High integrity Ada: The SPARK approach. Addison-Wesley, 1997.Google Scholar
- 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.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.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.K.A. Nyberg, editor. The annotated Ada Reference Manual. ANSI, 1983. ANSI/MIL-STD-1815A-1983.Google Scholar
- 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.SPARK — The SPADE Ada Kernel. Praxis Critical Systems, August 1997. Edition 3.3.Google Scholar
- 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