Bigraphs with sharing and applications in wireless networks

QA75 Electronic computers. Computer science

Sevegnani, Michele ; Calder, Muffy

University:University of Glasgow

Department:School of Computing Science

关键词: Bigraphs with sharing, wireless networks, formal methods, stochastic model checking, ubiquitous computing, process calculi, category theory, real-time verification;   

Others  :  http://theses.gla.ac.uk/3742/1/2012sevegnaniphd.pdf

来源: University of Glasgow

【 摘 要 】

Bigraphs are a fully graphical process algebraic formalism, capable of representing both the position in space of agents and their inter-connections. However, they assume a topologybased on sets of trees and thus cannot represent spatial locations that are shared among several entities in a simple or intuitive way. This is a problem, because shared locations are often a requirement, for example, when modelling scenarios in the physical world or in modern complex computer systems such as wireless networks and spatial-aware applications in ubiquitous computing.We propose bigraphs with sharing, a generalisation of the original definition of bigraphs, to allow for overlapping topologies. The new locality model is based on directed acyclic graphs.We demonstrate the new formalism can be defined in the general framework of bigraphical theories and wide reactive systems, as originally devised by Robin Milner. We do soby defining a categorical interpretation of bigraphs with sharing, an axiomatisation derived from the equations of a bialgebra over finite ordinals, and a normal form to expressbigraphical terms. We illustrate how sharing is essential for modelling overlapping localities by presenting two example case studies in the field of wireless networking. We show that bigraphs with sharing can be used realistically in a production environment by describing the implementation of an efficient matching algorithm and a software tool for the definition, simulation, visualisation and analysis of bigraphical reactive systems.