Abstract
The reliability of software is an increasingly important demand, especially for safety critical systems. RAISE is a mathematically based method which has been shown to be useful in the development of many kinds of software systems. However, RAISE has no particular features for specifying real-time requirements, which often occur in safety critical systems. Adding timing features to RAISE makes a new specification language, Timed RAISE Specification Language (TRSL), and gives it the power of specifying real-time applications. We then have to find a theoretical foundation for TRSL. In this paper, an operational semantics of TRSL is first introduced. Then we define a pre-order and test equivalence relation for TRSL. Some proof rules for TRSL are listed, and their soundness corresponding to our operational model is also explained.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
D. Bolignano, and M. Debabi.RSL: An Integration of Concurrent, Functional and Imperative Paradigms. Technical Report LACOS/BULL/MD/3/V12.48, 1993.
Jim Davies. Specification and Proof in Real-Time CSP. Distinguished Dissertation Series. Cambridge University Press, 1993.
M. Debabi. Intégration des paradigmes de programmation parallèle, fonctionnelle et impérative: fondements sémantiques. Ph.D. Thesis (Thèse de Doctorat en Informatique), Université Paris XI, Centre dx2019;Orsay, July 1994.
C. J. Fidge Specification and verification of Real-Time Behaviour Using Z and RTL in J. Vytopil (ed.), Proc FME’92, LNCS571 (Springer), 1992.
C. J. Fidge, I. J. Hayes and B. P. Mahony, Defining Differentiation and Integration in Z, Technical report 98-09, Software Verification Research Centre, School of Information Technology, The University of Queensland, September 1998.
Chris George and Xia Yong An Operational Semantics for Timed RAISE Technical Report No. 149, United Nations University/ International Institute for Software Technology, November 1998.
M. Hennessy and A. Ingólfsdóttir. Communicating Process with Value-passing and Assignments. In Formal Aspects of Computing, 1993.
Anne Haxthausen and Xia Yong A RAISE Specification Framework and Justification Assistant for the Duration Calculus. In ESSLLI-98 Workshop on Duration Calculus, August 1998.
Anne Haxthausen and Xia Yong. Linking DC together with TRSL. Research Report, Department of Information Technology, Technical University of Denmark, April 1999.
Li Li and He Jifeng Towards a Denotational Semantics of Timed RSL using Duration Calculus Technical Report No. 161, United Nations University/ International Institute for Software Technology, April 1999.
Z. Manna and A. Pnueli. Models of reactivity. In Acta Informatica. 30(7), 609–678, Springer-Verlag, 1993.
Anders P. Ravn. Design of Embedded Real Time Computing Systems. PhD thesis, Department of Computer Science, Technical University of Denmark, Denmark, September 1994.
The RAISE Language Group. The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int., 1992.
The RAISE Method Group. The RAISE Development Method. The BCS Practitioners Series. Prentice Hall Int., 1995.
Paritosh K. Pandya and Dang Van Hung. Duration Calculus of weakly monotonic time. Technical Report No. 122, United Nations University/ International Institute for Software Technology, September 1997.
Jifeng He, C.A.R. Hoare, Markus Müller-Olm, Ernst-Rüdiger Olderog, Michael Schenke, Michael R. Hansen, Anders P. Ravn, and Hans Rischel. The ProCoS Approach to the Design of Real-Time Systems: Linking Different Formalisms. In Formal Methods Europe 96, Oxford, UK, March 1996. Tutorial Material.
Qiu Zhongyan and Zhou ChaochenA Combination of Interval Logic and Linear Temporal Logic Technical Report No. 123, United Nations University/ International Institute for Software Technology, September 1997. An Operational Semantics for Timed RAISE 1027
Wang Yi. A Calculus of Real Time Systems. PhD thesis, Department of Computer Sciences, Chalmers University of Technology, Güterborg, Sweden, 1991
Zhou Chaochen and Michael R. Hansen. Chopping a point. In J. F. He et al (Eds.), BCS-FACS 7th Refinement Workshop, Electronic Workshops in Computing, Springer-Verlag, 1996.
Zhou Chaochen, C.A.R. Hoare and A.P. Ravn. A Calculus of Durations. Information Processing Letters, 40(5):269–276, 1991. Revised June 3, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yong, X., George, C. (1999). An operational semantics for timed RAISE. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_4
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive