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

在我们的社会中，分布式软件系统的广泛采用，包括物联网、视频会议和社交平台，或去中心化金融和加密货币，正在彻底改变全球数字基础设施和经济的格局。为了避免灾难，这些系统必须按照预期运行，即使在不断变化的环境条件、软件升级或意外事件（如故障或服务降级）下也是如此。为了获得对其预期行为的严格保证，对分布式系统进行正式验证是必不可少的。不幸的是，目前可用的正式模型只允许孤立地验证某些属性（例如，仅通信安全性，仅适应性），并且通过剥离分布式系统的显着特性（例如，无故障，无消息损坏，无延迟），大大简化了分布式系统的视图。此外，即使是正式模型也不能免除其元理论中的错误（例如，证明中的错误），从而导致后续的（新）理论，这是昂贵的，特别是当理论在编程语言或软件工具中实现时。该项目旨在填补这一空白，并开发Uni-pi，这是基于pi微积分和线性/会话类型的第一个统一的正式模型，用于验证安全性、适应性和弹性属性，同时保持一个现实的观点-我们将在这个项目中称之为-分布式软件生态系统存在故障、消息不一致或服务退化。此外，Uni-pi将被完全机械化，以获得一个构造正确的元理论。最后，我们将通过与我们的行业合作伙伴Actyx和RChain密切合作，并努力通过参与活动（如知识交流研讨会或技术峰会）建立新的联系，根据行业实践和案例研究来评估Uni-pi。该项目将为未来的新一代主流编程语言、软件工具和分布式生态系统奠定基础，这些语言、软件和生态系统将安全、适应性强、有弹性。

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.