Timed Process Algebras: A Tutorial
In this set of notes we give an overview of a particular approach to describing timed concurrent systems. The starting point is a well-developed semantic theory of process algebras based on testing. This consists of an operational semantics for a “time-free” process description language, a behavioural equivalence based on testing and an algebraic characterisation of this equivalence. We add to this language one timing construct, a time-out operator, and show how the theory can be extended to this time enriched language. This extended language is certainly restricted in its ability to describe timing phenomena but in the last section we show how it may be used as the basis for more expressive timed process description languages.
This extended language is certainly restricted in its ability to describe timing phenomena but in the last section we show how it may be used as the basis for more expressive timed process description languages.
KeywordsTransition System Clock Cycle Finite Subset Operational Semantic Proof System
Unable to display preview. Download preview PDF.
- [BB92]J. C. M. Baeten and J. A. Bergstra. Discrete time process algebra. Technical Report P9208, University of Amsterdam, 1992.Google Scholar
- [BG88]G. Berry and G. Gonthier. The synchronous programming language ESTEREL: design, semantics, implementation. Report 842, INRIA, Centre Sophia-Antipolis, Valbonne Cedex, 1988. To appear in Science of Computer Programming Google Scholar
- [Gro90]J.F. Groote. Specification and verification of real time systems in ACP. Report CS-R9015, CWI, Amsterdam, 1990. An extended abstract appeared in L. L.grippo, R.L. Probert and H. Ural, editors, Proceedings 10 t h International Symposium on Protocol Specification, Testing and Verification, Ottawa, pages 261–274, 1990.Google Scholar
- [Gue81]I. Guessarian. Algebraic Semantics. Lecture Notes in Computer Science vol 99, 1981.Google Scholar
- [Han91]Hans A. Hansson. Time and Probability in Formal Design of Distributed Systems. Ph.d. thesis, Uppsala University, 1991.Google Scholar
- [Hen88]M. Hennessy. An Algebraic Theory of Processes. MIT Press, 1988.Google Scholar
- [HI91]M. Hennessy and A. Ingolfsdottir. A theory of communicating processes with value-passing. Information and Computation, to appear, 1991.Google Scholar
- [Hoa85]C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
- [HR91]M. Hennessy and T. Regan. A process algebra for timed systems. Technical Report 5/91, CSAI, University of Sussex, 1991.Google Scholar
- [Lan89]R. Langerak. A testing theory for LOTOS using deadlock detection. In E. Brinksma, G. Scollo, and C.A. Vissers, editors, Proceedings of the Ninth International Conference on Protocol Specification, Testing and Verification, 1989.Google Scholar
- Lin91] H. Lin. Process Algebra Manipulator: User Guide. In K. Larsen, A. Skou (eds.), Proceedings of CAV91,Lecture Notes in Computer Science 575, Springer-Verlag 1991. Also Sussex Computer Science Tech. Rep. 9/91.Google Scholar
- [Mí189]R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
- MT90] F. Moller and C. Tofts. A temporal calculus of communicating systems. In Proc. Concur 90,pages 401–415. Springer-Verlag, 1990. LNCS 458.Google Scholar
- [MV89]S. Mauw and G.J. Veltink. An introduction to PSFa. In J. Diaz and F. Orejas, editors, TAPSOFT89, vol 2, volume 352 of Lecture Notes in Computer Science, pages 272–285, 1989.Google Scholar
- [NS90]X. Nicollin and J. Sifakis. The algebra of timed processes ATP: Theory and application. Technical Report RT-C26, Laboratoire de Génie Informatique de Grenoble, 1990. to appear in Information and Computation.Google Scholar
- [P1o81]G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.Google Scholar
- [Reg92]T. Regan. A Process Algebra for Real-Time Systems. Ph.d. thesis, University of Sussex, 1992.Google Scholar
- [Wan91]Wang Yi. A Calculus of Real Time Systems. Ph.D. thesis, Chalmers University, 1991.Google Scholar