What's on in Computing Science?

Date: Tuesday, 14 February, 2012
Time: 16:00
Location: Sir Alwyn Williams Building, 422 Seminar Room
[FATA talk] Real-time verification with bigraphs with sharing
Michele Sevegnani
Bigraphical reactive systems (BRS) is a recent formalism for modelling the temporal and spatial evolution of computation. A BRS consists of a set of bigraphs and a set of rewrite rules, the latter defines the evolution of the system by specifying how the set of bigraphs can be reconfigured. We have extended the standard formalism to bigraphs with sharing so that spatial locations can overlap. In this talk, we describe a novel application of formal modelling: on-line generation and analysis of formal models of the current network topology, network events and activated access policies. We model both spatial and temporal behaviour of network interactions using bigraphs with sharing. 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 based on checking predicates that detect undesirable network configurations, or configurations that violate policy constraints.

Contact: Dr Oana Andrei (oana.andrei@glasgow.ac.uk)

Add to my calendar