Abstract

Bigraphical reactive systems (BRS) is a formalism developed by Robin Milner for modelling the temporal and spatial evolution of computation. We have extended it to bigraphs with sharing so that spatial locations can overlap. In this talk, we describe a novel application for runtime verification of domestic wireless network management. We present on-line generation and analysis of bigraphical models of the current network topology, network events and activated access policies. The models are generated in real-time from events such as a new machine joining the network, or from policy activations such as blocking TCP traffic from a given site. Verification is carried out in real-time by a bespoke bigraph reasoning system.

BIO : I am a PhD student at the University of Glasgow, under Professor Muffy Calder. My research is on bigraphs with sharing and innovative applications of formal methods to every-day problems. I am involved in the Homework Research Project, developing new network architectures and management tools for future domestic networks. I obtained a BSc. degree in Computer Science from the University of Trento (thesis Encoding Orc in Pi-calculus) and an MSc in Informatics from the University of Edinburgh and Trento (thesis Implementing Stochastically-Timed COWS for the Prism Probabilistic Model Checker), supervised by Stephen Gilmore and Paola Quaglia.