© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Travelling processes
Xinbei Tang and Jim Woodcock
In Dexter Kozen, editor, MPC2004: The 7th International Conference on Mathematics of Program Construction, volume 3125 of Lecture Notes in Computer Science, pages 182-196, Stirling, Scotland, UK, July 2004. Springer-Verlag,.Abstract
This paper describes a refinement-based development method for mobile processes. Process mobility is interpreted as the assignment or communication of higher-order variables, whose values are process constants or parameterised processes, in which target variables update their values and source variables lose their values. The mathematical basis for the work is Hoare and He's Unifying Theories of Programming (UTP). In this paper, we present a set of algebraic laws and refinement laws to be used for the development of mobile systems. The correctness of these laws is ensured by the UTP semantics of mobile processes. We illustrate our theory through a simple example that can be implemented in both a centralised and a distributed way. First, we present the pi-calculus specification for both systems and demonstrate that they are observationally equivalent. Next, we show how the centralised system may be step-wisely developed into the distributed one using our proposed laws.
Bibtex Record
@inproceedings{1828,
author = {Xinbei Tang and Jim Woodcock},
title = {Travelling Processes},
month = {July},
year = {2004},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1828},
publication_type = {inproceedings},
submission_id = {11750_1079089495},
editor = {Dexter Kozen},
series = {Lecture Notes in Computer Science},
address = {Stirling, Scotland, UK},
publisher = {Springer-Verlag, },
booktitle = {MPC2004: The 7th International Conference on Mathematics of Program Construction},
volume = {3125},
}