Abstract
In this paper the most difficult step of a method is presented by which requirements in the duration calculus (DC) can be transformed into occam programs such that the implementation is correct by construction. Several rules for correct transformations from DC towards an important intermediate stage, the specification language SLtime, will be shown. In particular we shall explain the interplay between requirements and a control program, the introduction of parallelism and the change from the state based DC-description to the event based SLtimedescription.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J.C.M.Baeten, J.A.Bergstra. Real time process algebra. Formal Aspects of Computing 3(2), 1991, 142–188.
Zhou Chaochen, C.A.R.Hoare, A.P.Ravn. A Calculus of Durations. IPL 40(5), 1992, 269–276.
M.FrÄnzle. Proposal for a Programming Language Core for ProCoS II. ProCoS Project Document [MF 11/2], UniversitÄt Kiel.
M.R.Hansen, E.-R. Olderog, M. Schenke. et al. A Duration Calculus Semantics for Real-Time Reactive Systems. ProCoS Project Document [OLD MRH 1/1], UniversitÄt Oldenburg, 1993.
J.J.M.Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558 (Springer-Verlag, 1991).
P.C.Masiero, A.P.Ravn, H.Rischel. Refinement of Real Time Specifications. ProCoS Project Document [ID/DTH PCM/0.1], Lyngby.
C.Morgan. Programming from Specifications. Prentice Hall, 1990.
X.Nicollin, J.Sifakis, S.Yovine. From ATP to Timed Graphs and Hybrid Systems. REX 1991, LNCS 600 (Springer-Verlag, 1991), 549–572.
E.-R.Olderog. Interfaces between Languages for Communicating Systems. ICALP 1992, LNCS 623 (Springer-Verlag, 1992), 641–655, invited paper.
E.-R.Olderog,S. Rössig, J.Sander, M. Schenke. ProCoS at Oldenburg: The Interface between Specification Language and occam-like Programming Language. Technical Report Bericht 3/92, Univ. Oldenburg 1992.
A.P.Ravn, H.Rischel, K.M.Hansen. Specifying and Verifying Requirements of Real-Time Systems. IEEE Transactions on Software Engineering, vol. 19, 1 (1993) 41–55.
M.Schenke. A Timed Specification Language for Concurrent Reactive Systems. Workshop on the Semantics of Specification Languages, Utrecht 1993, Springer-Verlag, Workshops in Computing.
M.Schenke. Specification and Transformation of a Gas Burner. ProCoS Project Document [OLD MS 8/1], UniversitÄt Oldenburg, 1993.
D.Scholefield, H.Zehan, He Jifeng. A Specification Oriented Semantics for the Refinement of Real-Time Systems, to appear in Theoretical Computer Science 1994.
J.M.Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1989.
E.Zijlstra. The railroad crossing. Deliverable, Esprit project DESCARTES, Foxboro, The Netherlands, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schenke, M. (1994). Specification and transformation of reactive systems with time restrictions and concurrency. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_186
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_186
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58468-1
Online ISBN: 978-3-540-48984-9
eBook Packages: Springer Book Archive