Advertisement

A Formal Model of the Ada Ravenscar Tasking Profile; Protected Objects

  • Kristina Lundqvist
  • Lars Asplund
  • Stephen Michell
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1622)

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.

Keywords

Ada Tasking Protected Objects Ravenscar Formal Methods Run-Time System UPPAAL 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AD90]
    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.Google Scholar
  2. [Bar97]
    J. Barnes, “High Integrity Ada — The SPARK Approach”, Addison Wesley, ISBN 0-201-17517-7, 1997.Google Scholar
  3. [Bjo95]
    L. Björnfot, “Ada and Timed Automata”, In proc. Ada Europe, Frankfurt, Germany, LNCS 1031, pp. 389–405, Springer-Verlag, Oct 1995.CrossRefGoogle Scholar
  4. [Cha98]
    Pierre Chapront, “Ada+B The Formula for Safety Critical Software Development”, Ada Europe, Uppsala, Sweden, LNCS 1411, pp. 14–18, Springer-Verlag, June 1998.CrossRefGoogle Scholar
  5. [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.Google Scholar
  6. [DB98]
    B. Dobbing and A. Burns, “The Ravenscar Tasking Profile for High Integrity Real-Time Programs”, SIGAda’98, Nov 8–12, 1998.Google Scholar
  7. [FW96]
    S. Fowler and A. Wellings, “Formal Analysis of a Real-Time Kernel Specification”, FTRTFT’96, 1996Google Scholar
  8. [FW97]
    S. Fowler and A. Wellings, “Formal Development of a Real-Time Kernel”, 19th IEEE Real-Time Systems Symposium, Dec 1997.Google Scholar
  9. [GMP90]
    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.CrossRefGoogle Scholar
  10. [HRG98]
    ISO/IEC PDTR 15942, Guidance on the Use of the Ada Programming Language in High Integrity SystemsGoogle Scholar
  11. [HU79]
    J.E. Hopcroft and J.D. Ullman, “Introduction to Automata Theory, Languages and Computation”, ISBN 0-201-02988-X, Addison-Wesley, 1979.Google Scholar
  12. [Hut94]
    A. Hutcheon, “Safe Nucleus Formal Specification”, Project Reference CI/GNSR/27: The Design and Development of Safety Kernel, Aug 1994.Google Scholar
  13. [IRT99]
    To be published in Ada letters, spring 1999.Google Scholar
  14. [JM86]
    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.Google Scholar
  15. [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.zbMATHCrossRefGoogle Scholar
  16. [Smi92]
    M.K. Smith, The AVA Reference Manual: Derived from ANSI/MIL-STD-1815A-1983, Computational Logic Inc., Feb. 1992Google Scholar
  17. [Tol95]
    R.M. Tol, “Formal Design of a Real-Time Operating System Kernel”, Ph.D. thesis, University of Groningen, 1995.Google Scholar
  18. [WB97]
    A. Wellings and A. Burns, “Workshop Report”, The Eighth International Real-Time Ada Workshop (IRTAW8), Ada User Journal, vol 18, number 2, June 1997.Google Scholar

Copyright information

© SpringerVerlag 1999

Authors and Affiliations

  • Kristina Lundqvist
    • 1
  • Lars Asplund
    • 1
  • Stephen Michell
    • 2
  1. 1.Information Technology, Dept. of Computer SystemsUppsala UniversityUppsalaSweden
  2. 2.Maurya SoftwareOntarioCanada

Personalised recommendations