Abstract
The definition of the Ravenscar Tasking Profile for Ada95 provides a definition of a tasking runtime system with deterministic behaviour and low enough complexity to permit a formal description of the model. The complete model of the Protected Object portion of the Ravenscar Model is presented in Uppaal. Some important properties are verified such as timing of calls to protected procedure. This is the first time a part of an Ada run-time has been formally verified.
★
Funded Berlin Heidelberg by Swedish National Board for Industrial and Technical Development, Swedish Nuclear Power Inspection, and Swedish Defence Material Administration
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, and D. Dill, “Automata for Modeling Real-Time Systems”, Proceedings of the 17th International Colloquium on Automata, Languages and Programming, vol. 443, Springer-Verlag, 1990.
J. Barnes, “High Integrity Ada — The SPARK Approach”, Addison Wesley, ISBN 0-201-17517-7, 1997.
L. Björnfot, “Ada and Timed Automata”, In proc. Ada Europe, Frankfurt, Germany, LNCS 1031, pp. 389–405, Springer-Verlag, Oct 1995.
Pierre Chapront, “Ada+B The Formula for Safety Critical Software Development”, Ada Europe, Uppsala, Sweden, LNCS 1411, pp. 14–18, Springer-Verlag, June 1998.
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.
B. Dobbing and A. Burns, “The Ravenscar Tasking Profile for High Integrity Real-Time Programs”, SIGAda’98, Nov 8–12, 1998.
S. Fowler and A. Wellings, “Formal Analysis of a Real-Time Kernel Specification”, FTRTFT’96, 1996
S. Fowler and A. Wellings, “Formal Development of a Real-Time Kernel”, 19th IEEE Real-Time Systems Symposium, Dec 1997.
David Guaspari, Carla Marceau, and Wolfgang Polak. Formal Verification of Ada Programs. IEEE Transactions on Software Engineering, vol. 16, no. 9, September 1990, pp. 1058–1075.
ISO/IEC PDTR 15942, Guidance on the Use of the Ada Programming Language in High Integrity Systems
J.E. Hopcroft and J.D. Ullman, “Introduction to Automata Theory, Languages and Computation”, ISBN 0-201-02988-X, Addison-Wesley, 1979.
A. Hutcheon, “Safe Nucleus Formal Specification”, Project Reference CI/GNSR/27: The Design and Development of Safety Kernel, Aug 1994.
To be published in Ada letters, spring 1999.
F. Jahanian and A. K. Mok, “Safety analysis of timing properties in real-time systems”, IEEE Transactions on Software Engineering, 12(9):890–904, Sept. 1986.
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.
M.K. Smith, The AVA Reference Manual: Derived from ANSI/MIL-STD-1815A-1983, Computational Logic Inc., Feb. 1992
R.M. Tol, “Formal Design of a Real-Time Operating System Kernel”, Ph.D. thesis, University of Groningen, 1995.
A. Wellings and A. Burns, “Workshop Report”, The Eighth International Real-Time Ada Workshop (IRTAW8), Ada User Journal, vol 18, number 2, June 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 SpringerVerlag
About this paper
Cite this paper
Lundqvist, K., Asplund, L., Michell, S. (1999). A Formal Model of the Ada Ravenscar Tasking Profile; Protected Objects. In: González Harbour, M., de la Puente, J.A. (eds) Reliable Software Technologies — Ada-Europe’ 99. Ada-Europe 1999. Lecture Notes in Computer Science, vol 1622. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48753-0_2
Download citation
DOI: https://doi.org/10.1007/3-540-48753-0_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66093-4
Online ISBN: 978-3-540-48753-1
eBook Packages: Springer Book Archive