Abstract
We introduce a generalised notion of a real-time specification language (“GPLC-Automata”) that can be translated directly into real-time programs. In order to describe the behaviour of several GPLC-Automata implemented on one machine we introduce composition operators which form a process algebra. We give several algebraic laws and prove that each system is equivalent to a system in a certain normal form. Moreover, we demonstrate how a real-time specification in terms of GPLC-Automata can be decomposed into an untimed part and a timed part.
This research was partially supported by the Leibniz Programme of the German Research Council (DFG) under grant Ol 98/1-1.
Chapter PDF
References
R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In Fifth Annual IEEE Symp. on Logic in Computer Science, pages 414–425. IEEE Press, 1990.
R. Alur and D.L. Dill. A theory of timed automata. TCS, 126:183–235, 1994.
J.W. Davies and S.A. Schneider. A Brief History of Timed CSP. TCS, 138, 1995.
H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. In M. Bertran and T. Rus, editors, ARTS’97, volume 1231 of LNCS, pages 111–125, Mallorca, Spain, May 1997. Springer.
H. Dierks. Specification and Verification of Polling Real-Time Systems. PhD thesis, University of Oldenburg, July 1999.
H. Dierks. Synthesizing Controllers from Real-Time Specifications. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(1):33–43, 1999.
H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. In H. Rischel, editors. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of LNCS, Lyngby, Denmark, September 1998. Springer Ravn and Rischel [16], pages 29–40.
H. Dierks and J. Tapken. Tool-Supported Hierarchical Design of Distributed Real-Time Systems. In Proceedings of the 10th EuroMicro Workshop on Real Time Systems, pages 222–229. IEEE Computer Society, June 1998.
M.R. Hansen and Zhou Chaochen. Duration Calculus: Logical Foundations. Formal Aspects of Computing, 9:283–330, 1997.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. Information and Computation, 111:193–244, 1994.
B. Krieg-Brückner, J. Peleska, E.-R. Olderog, D. Balzer, and A. Baer. UniForM — Universal Formal Methods Workbench. In U. Grote and G. Wolf, editors, Statusseminar des BMBF Softwaretechnologie, pages 357–378. BMBF, Berlin, March 1996.
K.G. Larsen, P. Petterson, and Wang Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1+2):134–152, December 1997.
O. Maler and A. Pnueli. Timing Analysis of Asynchronous Circuits using Timed Automata. In Proc. CHARME’95, volume 987 of LNCS, pages 189–205. Springer, 1995.
O. Maler and S. Yovine. Hardware Timing Verification using Kronos. In Proc. 7th Conf. on Computer-based Systems and Software Engineering. IEEE Press, 1996.
X. Nicollin, J. Sifakis, and S. Yovine. Compiling Real-Time Specifications into Extended Automata. IEEE Transactions on Software Engineering, 18(9):794–804, September 1992.
A.P. Ravn and H. Rischel, editors. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of LNCS, Lyngby, Denmark, September 1998. Springer.
S.A. Schneider. An Operational Semantics for Timed CSP. Information and Computation, 116:193–213, 1995.
J. Tapken and H. Dierks. MOBY/PLC — Graphical Development of PLC-Automata. In H. Rischel, editors. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of LNCS, Lyngby, Denmark, September 1998. Springer Ravn and Rischel [16], pages 311–314.
S. Yovine. Kronos: a verification tool for real-time systems. Software Tools for Technology Transfer, 1(1+2):123–133, December 1997.
Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. IPL, 40/5:269–276, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dierks, H. (2000). A Process Algebra for Real-Time Programs. In: Maibaum, T. (eds) Fundamental Approaches to Software Engineering. FASE 2000. Lecture Notes in Computer Science, vol 1783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46428-X_6
Download citation
DOI: https://doi.org/10.1007/3-540-46428-X_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67261-6
Online ISBN: 978-3-540-46428-0
eBook Packages: Springer Book Archive