Advanced Model-Based Engineering and Reasoning
We're advancing computing systems through research and collaboration.
Our aims
The Advanced Model-Based Engineering and Reasoning (AMBER) group aims to help people design, develop, and verify advanced computing systems. The group achieves this by developing well-founded models, techniques, and tools.
The current group lead for AMBER is Jonte Hance.
Collaborators
We have extensive national and international collaborations with academia and industry. These collaborations have led to joint publications, industry co-productions, and research projects.
List of current collaborators
Our current collaborators include:
- Aarhus University
- Hiroshima University
- King’s College London
- Leiden University
- LMU Munich
- McMaster University
- Nicolaus Copernicus University in Torun
- Renesas Electronics
- University of Bristol
- University of Liverpool
- University of Manchester
- University of Oxford
- OCamlPro
We're developing collaborations with:
- Heriot-Watt University
- Kagawa University
- Kyoto University
- Microsoft
- Northumbria University
- Nagoya University
Case studies
4* Impact Case Study in REF 2021
Asynchronous electronic circuits have considerable advantages over traditional clocked circuits in Power Management Integrated Circuits (PMIC). But they are notoriously difficult to design correctly.
Our research, implemented in the WORKCRAFT software framework, significantly improved Dialog Semiconductor’s PMIC designs. The underlying technologies have also been applied by GitHub Inc. and Analog Devices Inc.
Contact: Professor Maciej Koutny
Download the case study (PDF: 65KB)
Visit the REF 2021 Computer Science and Informatics (UoA 11) page
The INTO-CPS project developed an integrated tool chain for the Model-Based Design of Cyber-Physical Systems
The tool chain supported the multidisciplinary, collaborative modelling of Cyber-Physical Systems from the requirements to hardware and software realisation. This ensured traceability throughout development.
Contact: Professor John Fitzgerald and Dr Ken Pierce
The INTO-CPS project has ended. The project has been transferred to the INTO-CPS Association.
Research areas
Fundamentals of modelling and verification 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
AMBER leads our research in the fundamentals of modelling and verification.
Research projects
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
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 Centre (SOC) team.
We also investigate novel discrete relational structures. We aim to develop interval order semantics of concurrent systems.
UNCOVER
Researcher: Professor Maciej Koutny
Funder: EPSRC
Funding amount: £559k
Duration: 2013-2016
The project developed theories and implemented prototype software tools. This is for the formal verification, synthesis and analysis of complex evolving systems. These may involve hardware, software and human organisations.
The group developed a rigorous methodology. A toolkit based on structured behavioural representations supported this work.
This reduced the cognitive complexity of large systems and the storage and computational resources.
Model-based engineering research
We’re developing the next generation of methods and tools to help engineers specify, verify and refine systems through rigorous modelling. We integrate them into advanced software design paradigms (self-adaptive systems or digital twins).
We apply our methods in domains such as:
- cyber-physical systems (railway systems)
- asynchronous circuits
- autonomous systems
- self-protecting systems
Our AMBER group leads our research in model-based engineering.
Research projects
Predictability of Rail Network Performance Using Co-simulation and FMI-based Strategies (PrePCo)
Researcher: Dr Ken Pierce
Funder: Network Rail
Funding amount: £399k
Duration: 2021-2024
The project supported Network Rail in identifying and managing performance variability on the rail network. The project developed a methodology for analysing and simulating performance variability.
The group used data science and the Functional Mock-up Interface (FMI). There was an emphasis on capturing and simulating human performance as a cause of variability.
Digital Innovation HUBs and Collaborative Platform for Cyber-Physical Systems (HUBCAP)
Researcher: Professor John Fitzgerald and Dr Ken Pierce
Funder: Horizon 2020
Funding amount: £398k
Duration: 2020-2022
HUBCAP aimed to lower barriers for SMEs to realise the potential of growing autonomy in cyber-physical systems. They accessed advanced model-based design technology and provided training and guidance.
It was built on a network of Digital Innovation Hubs in seven European countries, offering SMEs opportunities to:
- undertake experiments
- seek investment
- access expertise and training
- form new business links
The project ran several open calls to provide cascading funding to 92 SMEs to support these experiments.
It built a platform to allow businesses to offer models, tools and other assets, and permits for others. They were able to access these on a pay-per-use basis in a sandbox environment promoting collaboration and experimentation.
STRATA
Researcher: Professor Alexander Romanovsky and Professor Cliff Jones
Funder: EPSRC
Funding amount: £965k
Duration: 2016-2021
STRATA was a 'platform grant' that enabled us to continue collaborations with Professor Alan Burns (York) and Professor Alex Yakovlev (Newcastle Engineering).
The focus was on Trustworthy Ambient Systems. It included concerns about the resources such as power. Jones' collaboration with Alan Burns continues to produce publications.
Digital Environment for Collaborative Intelligent De-carbonisation (DECIDe)
Researcher: Dr Ken Pierce
Funder: Rail Systems Safety Board
Funding amount: £100k
Duration: 2019-2020
This project examined the technical feasibility of applying the Functional Mock-up Interface (FMI) and co-simulation methodology to support:
- rail decarbonisation
- application of this methodology through a cloud-based ‘marketplace’
- the associated organisational motivations, barriers and enablers
Program analysis research
We use formal verification techniques to ensure correctness and security in software programs. We use a variety of methods for program analysis, including:
- summary-based approaches
- rely-guarantee reasoning
- concurrent separation logic
- type systems
- bounded model checking
- abstract interpretation
- automated testing
Our AMBER group leads our program analysis research.
Research projects
TRUSTED: Security Summaries for Secure Software Development
Researcher: Dr Narges Khakpour
Funder: EPSRC
Funding amount: £919k
Duration: 2023-2026
This EPSRC funded project aims to protect software systems against supply chain attacks, by developing:
- formal static analysis techniques
- tools for secure software development
Separation and Interference
Researcher: Professor Cliff Jones
Funder: Leverhulme
Funding amount: £138k
Duration: 2019-2023
This project tackled recording the scientific history of research on formalisms for specifying and developing software that employs concurrency.
The Leverhulme Foundation funding was crucial because of the cross-disciplinary nature of such work.
Taming Concurrency
Researcher: Professor Cliff Jones
Funder: EPSRC
Funding amount: £643k
Duration: 2013-2019
Jones's research on 'rely/guarantee methods' continues to stimulate many researchers. This project enabled closer collaboration with research on 'concurrent separation logic', with a focus on heap variables.
AI4FM
Researcher: Professor Cliff Jones
Funder: EPSRC
Funding amount: £467k
Duration: 2010-2014
This project explored ways in which AI approaches could help the formal development of software. It took the approach of mining proof attempts to detect patterns in attacks on particular applications.
Once a few key lemmas were established relating to specific data structures and functions, they made automatic proof far more practical.
Research projects
Quantum Algorithms for Nonlinear Differential Equations (Quandie)
Researcher: Dr Nick Chancellor
Funder: EPSRC
Funding amount: £265k
Duration: 2023-2025
This EPSRC-funded project studies the application of quantum computing to nonlinear differential equations. There was a specific focus on those arising in fluid mechanics.
The potential for improvements on Lattice Boltzmann and smoothed particle hydrodynamics.
Quantum Enhanced and Verified Exascale Computing (QEVEC)
Researcher: Dr Nick Chancellor
Funder: EPSRC
Funding amount: £1m
Duration: 2020 – 2025
This EPSRC-funded project studies the potential applications of quantum computers as co-processors in high-performance computing environments.
The target applications are fluids and material simulations.
Feasibility Study on Quantum Optimization of Aircraft Container Loading
Researcher: Dr Nick Chancellor
Funder: Innovate UK
Funding amount: £271k
Duration: 2023-2024
This Innovate UK funded project assesses the feasibility of near-term quantum computers in solving aircraft logistics problems.
The study targets both gate model and annealing applications, working with Unisys as an industrial partner and the national quantum computing centre.
Developing Quantum Advantage by Understanding the Paradoxical Aspects of Measurement in Quantum Systems
Researcher: Jonte R Hance
Funder: EPSRC (Quantum Technologies Career Acceleration Fellowship)
Funding amount: £1.7 million