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.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
L. Asplund and B. Johnson and K. Lundqvist. Session summary: The Ravenscar profile and implementation issues. Ada Letters, XIX(2):12–14, 1999.
R. Alur and D. Dill. Automata for modeling real-time systems. In ICALP 1990, volume 443 of LNCS, pages 322–335. Springer-Verlag, 1990.
J.G.P. Barnes. High Integrity Ada: The Spark Approach. Addison-Wesley, 1997.
B. Brosgol. Session summary: Future of the Ada language and language changes such as the Ravenscar profile. Ada Letters, XXII(4):113–119, 2002.
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.
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.
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.
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.
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.
I.J. Hayes. Real-time program refinement using auxiliary variables. In FTRTFT2000, volume 1926 of LNCS, pages 170–184. Springer-Verlag, 2000.
C.B. Jones. Development Methods for Computer Programs Including a Notion of Interference. PhD thesis, Programming Research Group, The University of Oxford, 1981.
C.B. Jones. Interference resumed. Technical Report UMCS-91-5-1, Department of Computer Science, The University of Manchester, May 1991.
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.
K.G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. Software Tools for Technology Transfer, 1(1+2):134–152, 1997.
I. Lee and V. Gehlot. Language constructs for distributed real-time programming. In IEEE Real-Time Systems Symposium, pages 57–66. IEEE, 1985.
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.
T.-M. Lin and A. Burns. Annotations for RavenSPARK. Technical report, Department of Computer Science, The University of York, 2002.
K. Lundqvist and L. Asplund. A Ravenscar-compliant run-time kernel for safetycritical systems. Real-Time Systems, 24(1):29–54, 2003.
D. Naydich and D. Guaspari. Timing analysis by model checking. In LFM2000, pages 71–82, June 2000.
Timing analysis for model checking (working document). Technical report, Odyssey Research Associates, June 2001.
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.
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.
K. Stølen. Development of Parallel Programs on Shared Data-Structures. PhD thesis, Department of Computer Science, The University of Manchester, 1990.
S.T. Taft and R.A. Duff, editors. Ada 95 Reference Manual: Language and Standard Libraries, volume 1246 of LNCS. Springer-Verlag, 1997.
A.J. Wellings. Session summary: Status and future of the Ravenscar profile. Ada Letters, XXI(1): 5–8, 2001.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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