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

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

• 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS

Additional Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT

General Terms:
Design, Languages, Management, Theory