Abstract
In this paper we show that every real-time system specified in a certain subset of Duration Calculus [24] can be decomposed into an untimed system communicating with suitable timers. Both asynchronous and synchronous communication are considered.
This work was partially funded by the Leibniz Programme of the German Research Council (DFG) under grant Ol 98/1-1.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, D. Dill. A theory of timed automata. Theoret. Comput. Sci. 126, 1994, 283–235
J. Davies. Specification and Proof in Real-Time GSP. Cambridge University Press, 1993.
S. Dick, J. Peleska. A structural decomposition theorem for real-time CSP. Tech. Report, Univ. Bremen, in preparation, 1998.
H. Dierks. The production cell: A verified real-time system. In: B. Jonsson and J. Parrow Eds., Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’96), LNCS 1135 (Springer-Verlag, 1996) 208–227.
H. Dierks. PLC-automata: a new class of implementable real-time automata. In: M. Bertran and T. Rus Eds., Transformation-Based Reactive Systems Development. LNCS 1231 (Springer-Verlag, 1997) 111–125.
H. Dierks. Synthesising controllers from real-time specifications. In: Tenth International Symposium on System Synthesis (IEEE CS Press, September 1997) 126–133.
K. Engelhardt, W.-P. de Roever, Data Refinement (Book draft, 1997).
R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel Eds.. Hybrid Systems. LNCS 736 (Springer-Verlag, 1993)
M.R. Hansen, Zhou Chaochen, Duration Calculus: Logical Foundations. Formal Aspects of Computing 9 (1997) 283–330.
Jifeng He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.-R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn, and H. Rischel. Provably correct systems. In: W.-P. de Roever, J. Vytopil Eds.. Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 863 (Springer-Verlag, 1994) [16] 288–335.
C. Heitmeyer and D. Mandrioli Eds., Formal Methods for Real-Time Computing. Trends in Software, Vol.5, Wiley, 1996).
C.A.R. Hoare, Communicating Sequential Processes (Prentice Hall, 1985).
INMOS Ltd., OCCam 2 Reference Manual (Prentice Hall, 1988).
M. Joseph Ed.. Real-time Systems — Specification, Verification and Analysis (prentice Hall, 1996).
B. Krieg-Brückner, J. Peleska, E.-R. Olderog, D. Balzer, A. Baer. UniForM — Universal Formal Methods Workbench. In: U. Grote and G. Wolf Eds., Statusseminar des BMBF Softwaretechnologie (BMBF, Berlin, 1996) 357–377.
H. Langmaack, W.-P. de Roever, J. Vytopil Eds.. Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 863 (Springer-Verlag, 1994).
K.G. Larsen, B. Steffen, C. Weise. Countinuous modeling of real time and hybrid systems: from concepts to tools. To appear in Software Tools for Technology Transfer (STTT, Springer-Verlag).
C. Lewerentz, T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. LNCS 891 (Springer-Verlag, 1995).
E.-R. Olderog, A.P. Ravn, J.U. Skakkebæk. Refining system requirements to program specifications. In: D. Mandrioli Eds., Trends in Software, Vol.5, Wiley, 1996) [11] 107–134.
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.
A.P. Ravn. Design of Embedded Real-Time Computing Systems. Thesis for the Doctor of Technics. Technical Report ID-TR: 1995-170, Technical University of Denmark, 1995.
M. Schenke, E.-R. Olderog, Transformational design of real-time systems-part I: from requirements to program specifications. iTo appear in Acta Inform.
M. Schenke. Development of Correct Real-Time Systems by Refinement. Habilitation thesis, Univ. Oldenburg, 1997.
Zhou Chaochen, C.A.R. Hoare, A.P. Ravn. A calculus of durations. Information Processing Letters 40/5 1991, 269–276.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Olderog, ER., Dierks, H. (1998). Decomposing Real-Time Specifications. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_18
Download citation
DOI: https://doi.org/10.1007/3-540-49213-5_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65493-3
Online ISBN: 978-3-540-49213-9
eBook Packages: Springer Book Archive