Bigraphs: Modelling, Simulation, and Type Systems

We study how bigraphical reactive systems may be used for modelling and
simulating — in a manner controlled by sorts and types — global ubiquitous
computing. Ubiquitous computing was in the early 1990s envisioned by
Mark Weiser to be the third wave of computing (after mainframes, and then
personal computers), in which each person has many computers, receding
into the background, at his or her disposal. Global ubiquitous computing
has been identified internationally, indeed it is a UK Grand Challenge, as
one of the most important challenges for computing in the 21st century.
In mathematical modelling of real-life systems, we aim to gain a deeper
understanding of their behaviour by studying their essence. Concurrent
and mobile systems are notoriously hard to understand in their entirety
and thus to give guarantees about. The complexity increases when global
ubiquitous computing is considered, especially as systems become larger.
A key observation is the importance of understanding this new paradigm
before it is realised by technological advances, because trustworthiness will
be paramount, and theory is an important factor in achieving this. To this
end, computer simulations complement well mathematical methods.
In this dissertation we focus on context-aware computing— in particular
location-aware computing — which is at the core of ubiquitous computing.
Our point of origin is the theory of Bigraphs by Milner and co-workers.
Up until now it has been an open question whether Bigraphs is a suitable
a model for ubiquitous computing, for which we provide a partial answer.
The relevant literature is surveyed and Bigraphs challenged by modelling
and simulation of location systems. Plato-graphical models are developed
for more advanced modelling. Exploiting Bigraphs as a meta-model, and to
control models, we show how to develop inductive type systems for Bigraphs.
We expand the knowledge of what may be achieved with Bigraphs.