We can't find the internet
Attempting to reconnect
Something went wrong!
Hang in there while we get back on track
"Formal Modeling and Analysis of Distributed Systems" by Ankush Desai (Strange Loop 2022)
Learn how Ankush Desai's talk discusses using formal methods to improve system design and augment guardrails for system correctness.
- Formal methods can help reduce design-level bugs in production by creating a precise formal specification of the system.
- P is a high-level state machine-based programming language that allows developers to write their system design as communicating state machines.
- P can be used to reason about distributed systems and check their correctness, even in the presence of non-determinism.
- The main challenge in applying formal methods is the steep learning curve and the problem of scaling complex formal methods tools to real-world systems.
- The process of creating a formal model can deliver value even if the proof is not completed.
- Formal methods can help developers think about the assumptions they are making about other components in their system.
- P models each component of the system as a state machine that talks to other components, allowing for easy reasoning about system behavior.
- The checker in P uses state-of-the-art techniques to prioritize the search and explore the state space of the distributed system, finding hard-to-find concurrency and message-interleaving bugs faster.
- The correspondence between high-level abstraction and actual implementation is difficult and requires ongoing effort to keep the design and implementation in sync.
- Formal methods are not a substitute for existing guardrails, but can augment them to provide additional assurance of system correctness.
- Writing specifications as programs can help improve the quality of the system design.
- P is not a replacement for other formal methods tools, but rather a complementary approach that can be used in addition to other techniques.