Formal Modeling and Analysis of Distributed Systems

This talk presents formal methods for designing, implementing, testing, and monitoring distributed systems. It introduces the state machine-based P programming framework and shows how model checking can find deep bugs.

Syllabus

Intro
Programming Distributed Systems is Challenging!
Not uncommon to find bugs in production after deployment
Formal Methods to the Rescue!
Thinking abstractly, formally, above coding
Challenges with wide spread adoption of Formal Methods!
Formal Reasoning of S3 Strong Consistency Design using P
Two Phase Commit Protocol
P Tutorials and Documentation
Lessons Learned (P as a Thinking Tool)
Model Checking as a search problem
How to find deep bugs?