کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
431272 | 1441260 | 2011 | 15 صفحه PDF | دانلود رایگان |

We present a process algebra called TiMo in which timeouts of interactions and adaptable migrations in a distributed environment with explicit locations can be specified. Timing constraints allow to control the communication between co-located mobile processes, and a migration action with variable destination supports flexible movement from one location to another. The model of time is based on local clocks rather than a global clock.We provide a structural translation of TiMo into behaviourally equivalent high level timed Petri nets. As a result, we obtain a formal net semantics for timed interaction and migration which is both structural and allows one to deal directly with concurrency and causality.
► New process algebra with process migration and timeouts in distributed environment.
► Local clocks are used to control communication between co-located processes.
► Structural translation of process expressions into equivalent Petri nets.
► Petri net representation directly supports verification methods based on causality.
Journal: The Journal of Logic and Algebraic Programming - Volume 80, Issue 7, October 2011, Pages 377–391