Note: alphabetical order of authors means equal contributions.
When an asset fails in a critical air navigation service, how urgent
is a repair? If we repair within 1 hour, 2 hours, or n hours, how
does this affect the likelihood of service failure? Can a formal
model support assessing the impact, prioritisation, and scheduling
of repairs in the event of component failures, and forecasting of
maintenance costs? These are some of the questions posed to us by a
large organisation and here we report on our experience of
developing a stochastic framework to answer them. We define and
explore logic properties concerning the likelihood of service
failure within certain time bounds, forecasting maintenance costs,
and we introduce a new concept of envelopes of behaviour that
quantify the effect of the status of lower level components on
service availability. The resulting model is highly parameterised
and user interaction for experimentation is supported by a
lightweight, web-based interface.
Reference: Michele Sevegnani, and Muffy Calder. Stochastic model
checking for predicting component failures and service
availability IEEE Transactions on Dependable and Secure Computing
(2017).
This seminar will be divided in two parts. In the first, I will present a novel algorithm for the target counting problem based on Constraint Satisfaction Problem. In the second, I will introduce a systematic approach based on bigraphs for ensuring the requirements of resource-competing applications are satisfied by a Wireless Sensor Network both before deployment and at runtime.
While HCI has a long tradition of formally modelling task-based interactions with graphical user interfaces, there has been less progress in modelling emerging ubiquitous computing systems due in large part to their highly contextual nature and dependence on unreliable sensing systems. We present an exploration of modelling an example ubiquitous system, the Savannah game, using the mathematical formalism of bigraphs, which are based on a universal process algebra that encapsulates both dynamic and spatial behaviour of autonomous agents that interact and move among each other, or within each other. We establish a modelling approach based on four perspectives on ubiquitous systems - Computational, Physical, Human, and Technology - and explore how these interact with one another. We show how our model explains observed inconsistencies in user trials of Savannah, and then, how formal analysis reveals an incompleteness in design and guides extensions of the model and/or possible system re-design to resolve this.
Bigraphs were introduced by Robin Milner as a universal mathematical model for representing the spatial configuration of physical or virtual objects, their interaction capabilities and their temporal evolution. In my previous work, I have extended the theory to "bigraphs with sharing" to allow overlapping or intersecting spaces. In the first part of the talk, I will showcase four example applications of bigraphs with sharing: a wireless communication protocol, a management framework for domestic wireless networks, a strategic location-based pervasive mixed-reality game, and BigraphER, a set of tools providing an efficient implementation of computation, simulation, and visualisation for bigraphs. The second part of the talk will focus on current research: Formal analysis of multi-purpose sensor networks, Languages for programming IoT systems, Reachability and coverability in bigraphical reactive systems.
In this talk, I will argue that some deficiencies of current software engineering practice for IoT can be addressed by new frameworks and software tools based on the theory of bigraphs. Bigraphs were introduced by Robin Milner as a universal mathematical model for representing the spatial configuration of physical or virtual objects, their interaction capabilities and their temporal evolution. In my previous work, I have extended the theory to allow overlapping, or intersecting spaces. In the first part of the talk I will showcase three example applications of bigraphs: a wireless communication protocol, a run-time verification system for home-networks and a mixed-reality game. The second part of the talk will focus on current research: Service interoperability and compositionality, Automatic deployment and dynamic contextual reconfiguration, and Languages for programming IoT systems.
Bigraphical Reactive Systems (BRS) are a universal model of computation for the representation of interacting systems that evolve in both time and space. Bigraphs have been shown forming a category called symmetric partial monoidal category and their dynamic theory is defined in terms of rewriting and transition systems, which can be explained in a categorical setting by the notions of relative push-outs (RPOs) and idem push-outs (IPOs). A limitation of bigraphs is that the underlying model of location is a forest, which means there is no straightforward representation of locations that can overlap or intersect. In this talk, I will introduce bigraphs with sharing, an extension of bigraphs which solves this problem by defining the model of location as a directed acyclic graph, thus allowing a natural representation of overlapping or intersecting locations. I will give a complete presentation of the extended theory, including a categorical semantics, algebraic properties, a normal form and several essential procedures for computation.