School of Computing

Mobile Process in Unifying Theories

Xinbei Tang

Technical Report 1-04, University of Kent, Computing Laboratory, Canterbury, Kent CT2 7NF, January 2004.

Abstract

This report presents the initial work in the development of a theory of mobile processes in Circus, a language for describing state-based reactive systems. The mathematical basis for the work is Hoare and He's Unifying Theories of Programming (UTP), where the alphabetised relational calculus is used to provide a common framework for the semantics and refinement calculus of different programming paradigms.

As our first step, we study the denotational semantics of mobile processes in UTP. Process mobility is interpreted as the assignment or communication of higher-order variables, whose values are process constants or parameterised processes, in which the target variables update their values and the source variables lose their values. We then present a set of algebraic and refinement to be used for the development of mobile systems. The correctness of these laws can be 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 derived into the distributed one using our proposed laws.

By formalising mobile processes and studying their refinement laws in the same semantic framework of Circus, they can be included in Circus' refinement calculus to enhance Circus with the ability to develop networks of mobile processes.

Download publication 369 kbytes (PDF)

Bibtex Record

@techreport{1787,
author = {Xinbei Tang},
title = {{M}obile {P}rocess in {U}nifying {T}heories},
month = {January},
year = {2004},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1787},
    publication_type = {techreport},
    submission_id = {19724_1076085910},
    number = {1-04},
    address = {Canterbury, Kent CT2 7NF},
    institution = {University of Kent, Computing Laboratory},
}

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

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

Last Updated: 21/03/2014