EPSRC logo

Details of Grant 

EPSRC Reference: EP/X027309/1
Title: Uni-pi: safety, adaptability and resilience in distributed ecosystems, by construction
Principal Investigator: Dardha, Dr O
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Actyx AG RChain Cooperative
Department: School of Computing Science
Organisation: University of Glasgow
Scheme: New Investigator Award
Starts: 01 October 2023 Ends: 30 September 2026 Value (£): 409,562
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
24 Jan 2023 EPSRC ICT Prioritisation Panel January 2023 Announced
Summary on Grant Application Form
The pervasive adoption of distributed software systems in our society, including Internet of Things, videoconference and social platforms, or decentralised finance and cryptocurrency, is drastically changing the landscape of the global digital infrastructure and economy. To avoid catastrophe, it is imperative that these systems behave as intended, even under constantly changing environmental conditions, software upgrades, or unplanned events, such as failures or service degradation.

To obtain rigorous guarantees of their intended behaviour, formal verification of distributed systems is essential. Unfortunately, the formal models currently available only allow verification of some properties in isolation (e.g., only communication safety, only adaptability) and drastically simplify the view of distributed systems by stripping them of salient features (e.g., no failures, no message corruption, no delays). Additionally, even formal models are not exempt from errors in their meta-theory (e.g., errors in proofs), thus leading to subsequent (new) theories, which is costly especially when theories are implemented in programming languages or as software tools.

This project aims to fill this gap and develop Uni-pi, the first unified formal model based on the pi-calculus and linear/session types, for the verification of safety, adaptability and resilience properties, while maintaining a realistic view of-what we will call in this project-distributed software ecosystems in the presence of failures, message inconsistencies or service degradation. Furthermore, Uni-pi will be fully mechanised to obtain a correct-by-construction meta-theory. Lastly, we will evaluate Uni-pi against practices and case studies in industry, by working closely with our industrial partners Actyx and RChain and striving to build new connections via the engagement activities, such as Knowledge Exchange Workshops or tech summits.

This project will lay the foundations for a new generation of mainstream programming languages, software tools and distributed ecosystems of the future that are safe, adaptable, and resilient, by construction.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.gla.ac.uk