Unifying Theories of Mobile Channels

TL;DR

This paper develops a denotational semantics framework within UTP for modeling channel mobility in reactive processes, allowing channels to dynamically change during execution, which enhances the expressiveness of process models.

Contribution

It introduces a novel UTP-based denotational semantics for channel mobility, extending reactive process theory to include dynamic channel communication and movement.

Findings

Defined new healthiness conditions for mobile channels

Extended UTP semantics for CSP to incorporate channel mobility

Provided formal model ensuring correct use of mobile channels

Abstract

In this paper we present the denotational semantics for channel mobility in the Unifying Theories of Programming (UTP) semantics framework. The basis for the model is the UTP theory of reactive processes (precisely, the UTP semantics for Communicating Sequential Processes (CSP)), which is slightly extended to allow the mobility of channels: the set of actions in which a process is authorised to participate, originally static or constant (set during the process's definition), is now made dynamic or variable: it can change during the process's execution. A channel is thus moved around by communicating it via other channels and then allowing the receiving process to extend its alphabet with the received channel. New healthiness conditions are stated to ensure an appropriate use of mobile channels.