SPARK—an annotated Ada subset for safety-critical programming

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

SPARK—an annotated Ada subset for safety-critical programming

Full text

Pdf (1.05 MB)

Source

Annual International Conference on Ada archive
Proceedings of the conference on TRI-ADA '90 table of contents

Baltimore, Maryland, United States

Pages: 392 - 402

Year of Publication: 1990

ISBN:0-89791-409-0

Authors

Bernard Carré	Program Validation Ltd., 26 Queen's Terrace, Southampton SO1 1BQ, England
Jonathan Garnsworthy	Program Validation Ltd., 26 Queen's Terrace, Southampton SO1 1BQ, England

Sponsors

SIGADA: ACM Special Interest Group on Ada Programming Language
Baltimore SIGAda Chapter : Baltimore SIGAda Chapter

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 16, Downloads (12 Months): 51, Citation Count: 5

Additional Information:

references cited by collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/255471.255563 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Jean-Francois Bergeretti , Bernard A. Carré, Information-flow and data-flow analysis of while-programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.37-61, Jan. 1985 [doi>10.1145/2363.2366]
	2	Grady Booch, Software engineering with Ada, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1983
	3	Brendish, C. Concepts of control objectives and assurance levels in critical systems. Proceedings of Conference at Software Tools 87, London. Online Publications (Advanced Computing Series: 8), 67-73, 1987.
	4	Bromell, J.Y. and Sadlet, S.J. A strategy for the development of safety-critical software. In 'Achieving Safety and Reliability with Computer Systems', edited by B.K. Daniels, Elsevier Applied Science, 1-13, 1987.
	5	CarrY, B.A~, Jennings, T.J., Maclennan, F.J. and Farrow, P.F. SPARK- the SPADE Ada Kernel (second edition), 1989. Obtainable from Program Validation Ltd.
	6	CarrY, B.A., O'Neill, I.M., Clutterbuck, D.L. and Debney, C.W.: 'SPADE- the Southampton Program Analysis and Development Environment.' In Sommerville, I. (Ed): 'Software engineering environments', Peter Peregrinus, 1986, 129-134.
	7	D. L. Clutterbuck , B. A. Carré, The verification of low-level code, Software Engineering Journal, v.3 n.3, p.97-111, May 1988
	8	Dettmer, R.: 'Making software safer'. Review of the Institution of Electrical Engineers (I.E.E.), London, September 1988, 321-324.
	9	D. Guaspari , C. Marceau , W. Polak, Formal Verification of Ada Programs, IEEE Transactions on Software Engineering, v.16 n.9, p.1058-1075, September 1990 [doi>10.1109/32.58790]
	10	Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	11	David C. Luckham , Friedrich W. von Henke , Bernd Krieg-Brückner , Olaf Owe, ANNA: a language for annotating Ada programs, Springer-Verlag New York, Inc., New York, NY, 1987
	12	Neilan, P.J. The assessment of safety-related systems containing software, Proe. Centre for Software Reliability Conference on Certification, London 1988.
	13	O'Neill, I.M., Clutterbuck, D.L., Farrow, P.F., Summers, P.G. and Dolman, W.C.: 'The formal verification of safety-critical assembly code.' Proceedings of 'SAFE- COMP 88', IFAC/IFIP international Symposium on Safety-Related Computers, Fulda, November, 1988.
	14	Parkin, G.I. and O'Neill, G.: Specification of the MAA Standard in VDM. Report DITC 160/90, February 1990, National Physical Laboratory, Teddington, Middlesex TW11 0LW, U.K.
	15	J. M. Spivey, The Z notation: a reference manual, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989

CITED BY 5

	James Sutton , Bernard Carré, Ada: the cheapest way to build a line of business, Proceedings of the conference on TRI-Ada '95: Ada's role in global markets: solutions for a changing complex world, p.320-330, November 05-10, 1995, Anaheim, California, United States
	Dong-Ik Oh , T. P. Baker, Optimization of Ada '95 tasking constructs, Proceedings of the conference on TRI-Ada '97, p.79-88, November 09-13, 1997, St. Louis, Missouri, United States
	Tullio Vardanega, A case for exceptions, ACM SIGAda Ada Letters, v.XXI n.3, September 2001
	P. V. Bhansali, A systematic approach to identifying a safe subset for safety-critical software, ACM SIGSOFT Software Engineering Notes, v.28 n.4, July 2003
	Les Hatton, Language subsetting in an industrial context: A comparison of MISRA C 1998 and MISRA C 2004, Information and Software Technology, v.49 n.5, p.475-482, May, 2007

Collaborative Colleagues:

Bernard Carré: colleagues

Jonathan Garnsworthy: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player