A Calculus of Mobility and Communication for Ubiquitous Computing

Nosheen Gul
(University of Leicester, England)

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.

In Maurice H. ter Beek and Alberto Lluch Lafuente: Proceedings 11th International Workshop on Automated Specification and Verification of Web Systems (WWV 2015), Oslo, Norway, 23rd June 2015, Electronic Proceedings in Theoretical Computer Science 188, pp. 6–22.
Published: 14th August 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.188.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org