School of Computing

Towards mobile processes in unifying theories

Xinbei Tang and Jim Woodcock

In Jorge Cuellar and Zhiming Liu, editors, SEFM2004: the 2nd IEEE International Conference on Software Engineering and Formal Methods, pages 182-196, Beijing, China, September 2004. IEEE Computer Society Press. To appear.

Abstract

This paper presents a denotational semantics of mobile processes in Hoare \& He's Unifying Theories of Programming (UTP). Process mobility is captured by the mobile assignment or communication of higher-order variables, in which both the source and the target are process-valued variables. Processes are moved around in the system by updating the target and losing the value of the source. The semantics can be used to guarantee the correctness of a set of algebraic of refinement laws for the step-wise development of mobile systems. We give an outline of this development method, present and prove some of the laws.



Bibtex Record

@inproceedings{1939,
author = {Xinbei Tang and Jim Woodcock},
title = {Towards Mobile Processes in Unifying Theories},
month = {September},
year = {2004},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {To appear},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1939},
    publication_type = {inproceedings},
    submission_id = {14657_1090228786},
    booktitle = {SEFM2004: the 2nd IEEE International Conference on Software Engineering and Formal Methods},
    editor = {Jorge Cuellar and Zhiming Liu},
    address = {Beijing, China},
    publisher = {IEEE Computer Society Press.},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014