Abstract
This paper discusses the need for diversity in any development process used for high integrity software and describes some ways in which differing levels of diversity can be created. A summary of the SPARK language is given and experience with the use of SPARK in creating the highest level of diversity for safety critical software is described. Current best practice for the use of SPARK is then described as well as potential future developments in its use.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Defence Standard 00-55, The Procurement of Safety Related Software in Defence Equipment, Issue 2
Defence Standard 00-56, Safety Management Requirements for Defence Systems, Issue 2
IEEE SESC Software Safety Planning Group, Action Plan, 15 October 1996
Ricky W Butler and George B Finelli, The Infeasibility of Experimental Quantification of Life-Critical Software Reliability Proceedings of the ACM SIGSOFT'91 Conference on Software for Critical Systems, December 1991
Bev Littlewood and Lorenzo Strigini, Validation of Ultrahigh Dependability for Software-Based Systems, Communications of the ACM, Volume 36, No 11
SPARK — The SPADE Ada Kernel Edition 3.2, October 1996 available from Praxis Critical Systems
A Study of High Integrity Ada: Language Review, Study for UK MoD, Document Reference SLS31c/73-1-D, 9 July 1992
A Study of High Integrity Ada: Analysis of Ada Programs, Study for UK MoD, Document Reference SLS31c/73-2-D, 30 April 1993
Jacques Brygier and Marc Richard-Foy, Certification of Ada Real Time Executives for Safety Critical Applications Proceedings of Ada-Europe '93, Michel Gauthier (Ed), Springer-Verlag 1993
John Barnes (with Praxis Critical Systems), High Integrity Ada: The SPARK Approach, Addison Wesley Longman 1997
Mark Saaltink and Steve Michell, Ada 95 Trustworthiness Study: Analysis of Ada 95 for Critical Systems ORA Canada Technical Report, TR-96-5499-03a, January 1997
Bernard Carré, Jon Garnsworth and William Marsh, SPARK — A Safety-Related Ada Subset Proceedings of the 1992 Ada UK International Conference, October 1992, ‘Ada in Transition', WJ Taylor (Ed), IOS Press 1992
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thornley, J.P. (1997). Static analysis and diversity in the software development process — experiences with the use of SPARK. In: Hardy, K., Briggs, J. (eds) Reliable Software Technologies — Ada-Europe '97. Ada-Europe 1997. Lecture Notes in Computer Science, vol 1251. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63114-3_24
Download citation
DOI: https://doi.org/10.1007/3-540-63114-3_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63114-9
Online ISBN: 978-3-540-69150-1
eBook Packages: Springer Book Archive