Skip to main content

Mobile Process in Unifying Theories

Tang, Xinbei (2004) Mobile Process in Unifying Theories. Technical report. University of Kent, Canterbury, Kent CT2 7NF (KAR id:14219)

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: Reports and Papers (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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:02 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/14219 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.