P: Formal Modeling and Analysis of Distributed Systems

No ratings

Presented at High Confidence Software and Systems Conference 2022 by

Ankush Desai

Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about correctness in the presence of myriad possible interleaving of messages and failures. Unsurprisingly, it is common for service teams to uncover correctness bugs after deployment. Formal methods (FM) can play an important role in addressing this challenge. But the key requirement for "success" in an industrial setting would be the ability to integrate FM in all the phases of development process from system design, to implementation, to unit and integration testing, and even in production. In this talk, we will provide an overview of the P programming framework. We will discuss how P is currently being used extensively inside Amazon (AWS) to integrate principles of FM in to the development lifecycle of service teams and deliver complex distributed services with higher assurance of correctness. P is a state machine-based programming language for modeling and specifying complex distributed systems. Details about the P framework with tutorials and related publications can be found here: https://p-org.github.io/P/. P is an open-source tool with users and contributors from industry and academia. It would be great to through this talk engage with the industrial and adacemic community.