Abstract
We present a process algebra where timeouts of interactions and adaptable migrations in a distributed environment with explicit locations can be defined. Timing constraints allow to control the interaction (communication) between co-located mobile processes, and a migration action with variable destination supports flexible movement from one location to another. We define an operational semantics, and outline a structural translation of the proposed process algebra into operationally equivalent finite high level timed Petri nets. The purpose of such a translation is twofold. First, it yields a formal semantics for timed interaction and migration which is both compositional and allows to deal directly with concurrency and causality. Second, it should facilitate the use of simulation and verification tools developed within the area of Petri nets.
Chapter PDF
Similar content being viewed by others
Keywords
References
Aceto, L., Murphy, D.: Timing and Causality in Process Algebra. Acta Informatica 33, 317–350 (1996)
Aman, B., Ciobanu, G.: Mobile Ambients with Timers and Types. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 50–63. Springer, Heidelberg (2007)
Berger, M.: Basic Theory of Reduction Congruence forTwo Timed Asynchronous π-Calculi. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 115–130. Springer, Heidelberg (2004)
Bergstra, J.A., Klop, J.W.: Process Theory based on Bisimulation Semantics. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 50–122. Springer, Heidelberg (1989)
Best, E., Fraczak, W., Hopkins, R.P., Klaudel, H., Pelz, E.: M-nets: an Algebra of High Level Petri Nets, with an Application to the Semantics of Concurrent Programming Languages. Acta Informatica 35, 813–857 (1998)
Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. In: EATCS Monographs on TCS, Springer, Heidelberg (2001)
Bettini, L., et al.: The KLAIM Project: Theory and Practice. In: Priami, C. (ed.) GC 2003. LNCS, vol. 2874, Springer, Heidelberg (2003)
Cardelli, L., Gordon, A.: Mobile Ambients. Teoretical Computer Science 240, 170–213 (2000)
Christensen, S., Hansen, N.D.: Coloured Petri Nets Extended with Place Capacities, Test Arcs and Inhibitor Arcs. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, Springer, Heidelberg (1993)
Ciobanu, G., Prisacariu, C.: Timers for Distributed Systems. Electronic Notes in Theoretical Computer Science 164, 81–99 (2006)
Corradini, F.: Absolute Versus Relative Time in Process Algebras. Information and Computation 156, 122–172 (2000)
Devillers, R., Klaudel, H., Koutny, M.: A Petri Net Semantics of a Simple Process Algebra for Mobility. Electronic Notes in Theoretical Computer Science 154, 71–94 (2006)
Devillers, R., Klaudel, H., Koutny, M., Pommereau, F.: Asynchronous Box Calculus. Fundamenta Informaticae 54, 295–344 (2003)
Gorrieri, R., Roccetti, M., Stancampiano, E.: A Theory of Processes with Durational Actions. Theoretical Computer Science 140, 73–94 (1995)
Hennessy, M., Regan, T.: A Process Algebra for Timed Systems. Information and Computation 117, 221–239 (1995)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Jensen, K., Rozenberg, G. (eds.): High-level Petri Nets. Theory and Application. Springer, Heidelberg (1991)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press, Cambridge (1999)
Moller, F., Tofts, C.: A temporal Calculus of Communicating Systems. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 401–415. Springer, Heidelberg (1991)
Niaouris, A.: An Algebra of Petri Nets with Arc-Based Time Restrictions. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 447–462. Springer, Heidelberg (2005)
Starke, P.: Some Properties of Timed Nets under the Earliest Firing Rule. In: Rozenberg, G. (ed.) APN 1989. LNCS, vol. 424, Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciobanu, G., Koutny, M. (2008). Modelling and Verification of Timed Interaction and Migration. In: Fiadeiro, J.L., Inverardi, P. (eds) Fundamental Approaches to Software Engineering. FASE 2008. Lecture Notes in Computer Science, vol 4961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78743-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-78743-3_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78742-6
Online ISBN: 978-3-540-78743-3
eBook Packages: Computer ScienceComputer Science (R0)