Note: alphabetical order of authors means equal contributions.
As Open Radio Access Networks (O-RAN) adoption continues to
expand, AI/ML-driven applications (xApps) are increasingly
being deployed to enhance and simplify network management.
One of the main drivers for utilising AI is its
effectiveness in dealing with the complexity and the rapidly
evolving nature of real-world network environments. While
these approaches show promising results in many scenarios,
AI-based management applications can introduce new critical
challenges that traditional models did not face. One example
is the risk of misconfiguration by introducing logical
inconsistencies when trying to balance between availability,
QoS, and power efficiency.
An emerging trend in this area is the application of formal
verification to address these challenges by providing mathematical
guarantees on the behaviour of deployed systems. An established
technique used in the past primarily for the development of
high-assurance software, its more recent evolution to support
stochastic analysis has enabled its application to whole system
analysis in domains such as reliability of cyber-physical systems and
verification of wireless protocols.
In this talk, we present ongoing work of applying formal
verification to two O-RAN scenarios: safeguarding resource allocation
optimisation xApps generated by Large Language Models (LLMs) and
computing optimal thresholds between energy efficiency and service
availability using the PRISM model checker.
This work is part of CHEDDAR, the flagship UK hub dedicated to advancing future communications.
Bigraphs are an expressive graphical modelling formalism to represent systems that have both spatial aspects, e.g. a Person in a Room, and non-local aspects, e.g. communication between Person entities in (possibly) different Rooms. In fact, they are sometimes too expressive: allowing nonsense models to be created, for example where a Room is nested inside a Person! This talk explores "sorting schemes" for bigraphs which filter badly formed models in a similar way to how type systems filter badly formed programs. We show a language for specifying sorts, rules for verifying the well-sortedness of models, and many sorts of applications.
Bigraphs are an expressive modelling formalism, first introduced by Robin Milner, to model systems with strong notions of space and mobility. This talk informally introduces bigraphs---including their diagrammatic notation and gives some context around their development. We then give a high-level overview of some high-level overview of some of applications we have used them for before, some of the research and development undertaken at Glasgow including the state of the art BigraphER tool, and give some hints for where we might take bigraphs in the future.
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.