Fundamentals of Modelling and Verification Research
We're advancing research in modelling and verification, focussing on complex system behaviour.
Our research
We develop advanced formalisms to specify system behaviour, addressing complexities such as:
- concurrency
- uncertainty
- continuous or hybrid behaviour
Our research includes designing scalable methods to verify these models, using:
- compositional and modular techniques
- trustworthy AI-enabled techniques
Our Advanced Model-Based Engineering and Reasoning (AMBER) group leads our research in the fundamentals of modelling and verification.
National Edge AI Hub for Real Data
- Project: National Edge AI Hub for Real Data: Edge Intelligence for Cyber-disturbances and Data Quality
- Researcher: Professor Maciej Koutny
- Funder: EPSRC
- Funding amount: £15m
- Duration: 2024 – 2029
The Hub will address two challenges introduced by edge computing (EC) to support emerging AI algorithms:
- dealing with cyber disturbances
- managing data quality
The Hub will achieve these through a unique 3x3x3x2 matrix that reflects the complexity of these systems:
- three real-world application domains
- three tiers of EC architecture
- three ground-breaking research work streams
- two industry engagement work streams
Applications include autonomous electric vehicles, energy security and remote healthcare.
Folding groups, monoids and complexes with applications to step traces
- Project: Folding groups, monoids and complexes with applications to step traces
- Researcher: Professor Maciej Koutny
- Funder: Leverhulme Trust
- Funding amount: £299k
- Duration: 2022 – 2025
Our focus is on developing theories and algorithms concerned with step traces. This was undertaken by the Security Operations Center (SOC) team.
We also investigate novel discrete relational structures aimed at developing interval order semantics of concurrent systems.
UNCOVER
- Project: UNCOVER
- Researcher: Professor Maciej Koutny
- Funder: EPSRC
- Funding amount: £559k
- Duration: 2013 – 2016
The project aimed to develop theories and implement prototype software tools for the formal verification, synthesis and analysis of complex evolving systems which may involve hardware, software and human organisations.
The project developed a rigorous methodology supported by a toolkit based on structured behavioural representations.
The effective use of such representations greatly reduces the cognitive complexity of large systems and the storage and computational resources involved in the modelling and manipulation.
