Mobile Process in Unifying Theories

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.