Denotational semantics of channel mobility in UTP-CSP

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 extended to allow the mobility of channels—the set of channels that a process can use for communication (its interface), 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 interface with the received channel. We introduce a new concept, the capability of a process, which allows separating the ownership of channels from the knowledge of their existence. Mobile processes are then defined as having a static capability and a dynamic interface. Operations of a mobile telecommunications network, e.g., handover, load balancing, are used to illustrate the semantics. We redefine CSP operators and in particular provide the first semantics for the renaming and hiding operators in the context of channel mobility.