A formal model of the Ada Ravenscar tasking profile; delay until

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A formal model of the Ada Ravenscar tasking profile; delay until

Full text

Pdf (504 KB)

Source

Annual International Conference on Ada archive
Proceedings of the 1999 annual ACM SIGAda international conference on Ada table of contents

Redondo Beach, California, United States

Pages: 15 - 21

Year of Publication: 1999

ISBN:1-58113-127-5

Also published in ...

Authors

Kristina Lundqvist	Uppsala University, Information Technology, Dept. of Computer Systems, P.O. Box 325, S-751 05 Uppsala, Sweden
Lars Asplund	Uppsala University, Information Technology, Dept. of Computer Systems, P.O. Box 325, S-751 05 Uppsala, Sweden

Sponsors

SIGCAS: ACM Special Interest Group on Computers and Society
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGSOFT: ACM Special Interest Group on Software Engineering
SIGAPP: ACM Special Interest Group on Applied Computing
SIGPLAN: ACM Special Interest Group on Programming Languages
SIGBIO: ACM Special Interest Group on Biomedical Computing
SIGCSE: ACM Special Interest Group on Computer Science Education

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 16, Citation Count: 4

Additional Information:

abstract references cited by index terms 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/319294.319298 What is a DOI?

ABSTRACT

The definition of the Ravenscar Tasking Profile for Ada 95 provides a definition of a tasking runtime system with deterministic behaviour and low enough complexity to permit a formal description and verification of the model. A complete run-time system is being modeled using the real-time model checker UPPAAL, and this work describes the handling of delay until. Since scheduling is not yet modelled a simple non-preemptive scheduler has been used when verifying the delay queue.

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.

	AD90	Rajeev Alur , D. L. Dill, Automata for modeling real-time systems, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.322-335, July 1990, Warwick University, England
	ARM95	Intermetrics, "Ada95 Reference Manual", ISO/IEC-8652:1995, 1995.
	Bar97	J. Barnes, "High Integrity Ada- The SPARK Approach'', Addison Wesley, ISBN 0-201-17517-7, 1997.
	Bjo95	Lars Björnfot, Ada and Timed Automata, Proceedings of the Second International Eurospace - Ada-Europe Symposium on Ada in Europe, p.389-405, October 02-06, 1995
	Cha98	Pierre Chapront, Ada+B The Formula for Safety Critical Software Development, Proceedings of the 1998 Ada-Europe International Conference on Reliable Software Technologies, p.13-18, June 08-12, 1998
	CO+95	j. Crow, S.Owre, J. Rushby, N. Shankar, and M. Srivas, "A tutorial introduction to PVS", WIFT'95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995.
	DB98	Brian Dobbing , Alan Burns, The Ravenscar tasking profile for high integrity real-time programs, Proceedings of the 1998 annual ACM SIGAda international conference on Ada, p.1-6, November 08-12, 1998, Washington, D.C., United States
	FW96	Simon Fowler , Andy J. Wellings, Formal Analysis of a Real-Time Kernel Specification, Proceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.440-458, September 09-13, 1996
	FW97	S. Fowler , A. Wellings, Formal development of a real-time kernel, Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), p.220, December 03-05, 1997
	GMP90	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]
	HRG98	ISO/IEC PDTR 15942, Guidance on the Use of the A da Programming Language in High Integrity Systems,
	HU79	John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	Hut94	A. Hutcheon, "Safe Nucleus Formal Specification", Project Reference CI/GNSR/27: The Design and Development of Safety Kernel, Aug 1994.
	IRT99	To be published in Ads letters, spring 1999.
	JM86	F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
	LA99	K. Lundqvist, and L. Asplund, "A Formal Model of a Ravenscar-Compliant Run-Time Kernel and Application Code", Technical Report 1999-002, Department of Information Technology, Uppsala University, May 1999.
	LAM99	Kristina Lundqvist , Lars Asplund , Stephen Mitchell, A Formal Model of the Ada Ravenscar Tasking Profile; Protected Objects, Proceedings of the 1999 Ada-Europe International Conference on Reliable Software Technologies, p.12-25, June 07-11, 1999
	LPY97	K.G. Larsen, P. Pettersson, and W. Yi, "UPPAAL in a Nutshell", Int. Journal on Software Tools for Technology Transfer, Springer-Verlag, vol 1, number 1-2, pp. 134-152, Oct 1997.
	Smi92	M.K. Smith, The AVA Reference Manual: Derived from ANSI/MIL-STD-1815A-1983, Computational Logic Inc., Feb. 1992
	Tol95	R.M. Tol, "Formal Design of a Real-Time Operating System Kernel", Ph.D. thesis, University of Groningen, 1995.
	WB97	A. Wellings and A. Burns, "Workshop Report", The Eighth International Real-Time Ada Workshop (IRTAWS), Ads User Journal, vol 18, number 2, June 1997.

CITED BY 4

	Kristina Lundqvist , Lars Asplund, A Ravenscar-Compliant Run-time Kernel for Safety-Critical Systems*, Real-Time Systems, v.24 n.1, p.29-54, January 2003
	Douglas J. Howe , Stephen Michell, An approach to formal verication of real time concurrent Ada programs, ACM SIGAda Ada Letters, v.XXIII n.4, p.87-92, December 2003
	Tobias Amnell , Gerd Behrmann , Johan Bengtsson , Pedro R. D'Argenio , Alexandre David , Ansgar Fehnker , Thomas Hune , Bertrand Jeannet , Kim G. Larsen , M. Oliver Möller , Paul Pettersson , Carsten Weise , Wang Yi, UPPAAL: now, next, and future, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Lars Asplund , Kristina Lundqvist, Safety critical systems based on formal models, ACM SIGAda Ada Letters, v.XX n.4, p.32-39, Dec., 2000