Skip to main content
SpringerLink
Log in

Adding Temporal Annotations and Associated Verification to the Ravenscar Profile

  • Conference paper
  • First Online:
Reliable Software Technologies — Ada-Europe 2003 (Ada-Europe 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2655))

Included in the following conference series:

Abstract

This paper presents a proposal for extending the Ravenscar Tasking Profile with annotations that can be used to express temporal properties. An approach using model checking for the verification of compliance to the annotations is also presented. An extended example is used to illustrate the application of the proposed approach.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Asplund and B. Johnson and K. Lundqvist. Session summary: The Ravenscar profile and implementation issues. Ada Letters, XIX(2):12–14, 1999.

    Article  Google Scholar 

  2. R. Alur and D. Dill. Automata for modeling real-time systems. In ICALP 1990, volume 443 of LNCS, pages 322–335. Springer-Verlag, 1990.

    Google Scholar 

  3. J.G.P. Barnes. High Integrity Ada: The Spark Approach. Addison-Wesley, 1997.

    Google Scholar 

  4. B. Brosgol. Session summary: Future of the Ada language and language changes such as the Ravenscar profile. Ada Letters, XXII(4):113–119, 2002.

    Article  Google Scholar 

  5. A. Burns. How to verify a safe real-time system: The application of model checking and timed automata to the production cell case study. Real-Time Systems, 24(2):135–151, 2003.

    Article  MATH  Google Scholar 

  6. A. Burns, B. Dobbing, and G. Romanski. The Ravenscar tasking profile for high integrity real-time programs. In Ada-Europe 98, volume 1411 of LNCS, pages 263–275. Springer-Verlag, 1998.

    Google Scholar 

  7. A. Burns, B. Dobbing, and T. Vardanega. Guide for the use of the Ada Ravenscar profile in high integrity systems. Technical Report YCS 348, Department of Computer Science, The University of York, 2003.

    Google Scholar 

  8. C.J. Fidge, I.J. Hayes, and G. Watson. The deadline command. IEEE Software — Special Issue on Real-Time Systems, 146(2):104–111, 1999.

    Google Scholar 

  9. R. Gerber and S. Hong. Compiling real-time programs with timing constraint refinement and structure code motion. IEEE Transactions on Software Engineering, 21(5):389–404, May 1995.

    Article  Google Scholar 

  10. I.J. Hayes. Real-time program refinement using auxiliary variables. In FTRTFT2000, volume 1926 of LNCS, pages 170–184. Springer-Verlag, 2000.

    Google Scholar 

  11. C.B. Jones. Development Methods for Computer Programs Including a Notion of Interference. PhD thesis, Programming Research Group, The University of Oxford, 1981.

    Google Scholar 

  12. C.B. Jones. Interference resumed. Technical Report UMCS-91-5-1, Department of Computer Science, The University of Manchester, May 1991.

    Google Scholar 

  13. C.B. Jones. Reasoning about interference in an object-based design method. In FME’93, volume 670 of LNCS, pages 1–18. Springer-Verlag, 1993.

    Google Scholar 

  14. K.G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. Software Tools for Technology Transfer, 1(1+2):134–152, 1997.

    Article  MATH  Google Scholar 

  15. I. Lee and V. Gehlot. Language constructs for distributed real-time programming. In IEEE Real-Time Systems Symposium, pages 57–66. IEEE, 1985.

    Google Scholar 

  16. A. Leung, K. Palem, and A. Pnueli. TimeC: A time constraint language for ILP processor compilation. In The 5th Australian Conference on Parallel and Real Time Systems, pages 57–71. Springer-Verlag, 1998.

    Google Scholar 

  17. T.-M. Lin and A. Burns. Annotations for RavenSPARK. Technical report, Department of Computer Science, The University of York, 2002.

    Google Scholar 

  18. K. Lundqvist and L. Asplund. A Ravenscar-compliant run-time kernel for safetycritical systems. Real-Time Systems, 24(1):29–54, 2003.

    Article  MATH  Google Scholar 

  19. D. Naydich and D. Guaspari. Timing analysis by model checking. In LFM2000, pages 71–82, June 2000.

    Google Scholar 

  20. Timing analysis for model checking (working document). Technical report, Odyssey Research Associates, June 2001.

    Google Scholar 

  21. P. Pettersson. Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis, Department of Computer Systems, Uppsala University, February 1999.

    Google Scholar 

  22. E.W. Stark. A proof technique for rely/guarantee properties. In FST & TCS 85, volume 206 of LNCS, pages 369–391, New Dehli, 1985. Springer-Verlag.

    Google Scholar 

  23. K. Stølen. Development of Parallel Programs on Shared Data-Structures. PhD thesis, Department of Computer Science, The University of Manchester, 1990.

    Google Scholar 

  24. S.T. Taft and R.A. Duff, editors. Ada 95 Reference Manual: Language and Standard Libraries, volume 1246 of LNCS. Springer-Verlag, 1997.

    Google Scholar 

  25. A.J. Wellings. Session summary: Status and future of the Ravenscar profile. Ada Letters, XXI(1): 5–8, 2001.

    Article  Google Scholar 

  26. P.J. Whysall and J.A. McDermid. Object oriented specification and refinement. In 4th Refinement Workshop, Workshops in Computing, pages 150–184. Springer-Verlag, 1991.

    Google Scholar 

  27. J.C.P. Woodcock and B. Dickinson. Using VDM with rely and guarantee conditions: Experiences of a real project. In VDM’88, volume 328 of LNCS, pages 434–458. Springer-Verlag, 1988.

    Google Scholar 

  28. Q. Xu, W-P. Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149–174, 1997.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Real-Time Systems Research Group, Department of Computer Science, The University of York, Heslington, York, YO10 5DD, UK

    Alan Burns & Tse-Min Lin

Authors
  1. Alan Burns
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tse-Min Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Adalog, 19-21 rue du 8 mai 1945, 94110, Arcueil, France

    Jean-Pierre Rosen

  2. Software Engineering Laboratory, Swiss Federal Institute of Technology Lausanne, 1015, Lausanne EPFL, Switzerland

    Alfred Strohmeier

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Burns, A., Lin, TM. (2003). Adding Temporal Annotations and Associated Verification to the Ravenscar Profile. In: Rosen, JP., Strohmeier, A. (eds) Reliable Software Technologies — Ada-Europe 2003. Ada-Europe 2003. Lecture Notes in Computer Science, vol 2655. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44947-7_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-44947-7_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40376-0

  • Online ISBN: 978-3-540-44947-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation