| 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: |
|
| 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 Date | Panel Name | Outcome |
|
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
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| 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 |