A Calculus of Mobility and Communication for Ubiquitous Computing

TL;DR

This paper introduces CMC, a calculus for modeling mobility, communication, and context-awareness in ubiquitous computing, combining features of ambient calculus and global communication.

Contribution

It presents a novel calculus integrating mobility, communication, and context-awareness with formal semantics and behavioral equivalence, demonstrated through case studies.

Findings

Semantics of CMC coincide with reduction semantics

Behavioral equivalence via barbed bisimulation is established

Expressiveness shown through two case studies

Abstract

We propose a Calculus of Mobility and Communication (CMC) for the modelling of mobility, communication and context-awareness in the setting of ubiquitous computing. CMC is an ambient calculus with the in and out capabilities of Cardelli and Gordon's Mobile Ambients. The calculus has a new form of global communication similar to that in Milner's CCS. In CMC an ambient is tagged with a set of ports that agents executing inside the ambient are allowed to communicate on. It also has a new context-awareness feature that allows ambients to query their location. We present reduction semantics and labelled transition system semantics of CMC and prove that the semantics coincide. A new notion of behavioural equivalence is given by defining capability barbed bisimulation and congruence which is proved to coincide with barbed bisimulation congruence. The expressiveness of the calculus is illustrated by two case studies.