Uni-pi: safety, adaptability and resilience in distributed ecosystems, by construction

点击翻译按钮获取中文摘要

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.