Mobile Process in Unifying Theories

Tang, Xinbei (2004) Mobile Process in Unifying Theories. Technical report. University of Kent, Canterbury, Kent CT2 7NF (Full text available)

PDF
Download (378kB)
[img]
Preview

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.

Item Type: Monograph (Technical report)
Additional information: Technical Report 1-04
Uncontrolled keywords: mobile process, refinement, UTP, higher-order programming
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:02
Last Modified: 06 Sep 2011 01:26
Resource URI: http://kar.kent.ac.uk/id/eprint/14219 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year