Modeling and Verification of Concurrent & Distributed systems by Nikhil Barthwal - JOTB23

The majority of Distributed systems are designed as untestable whiteboard drawings. This leads to design flaws that go unnoticed. Human intuition has its limits and these systems operate beyond those limits. This talk describes how we can use mathematical models and to find & eliminate these flaws.
Distributed & concurrent systems have grown exponentially in popularity in recent years. However, the vast majority of these systems are designed as untestable whiteboard drawings. This leads to fundamental design flows that go unnoticed in the design phase leading to hard-to-find bugs that are expensive to correct.
This talk is about TLA+, a high-level language used for modelling concurrent & distributed systems using simple mathematics. These models can be thought of as blueprint design of software except it is exhaustively-testable.
Human intuition has its limits and most of these systems operate at a scale which is well beyond what we humans can comprehend. TLA+ specifications are written in formal language and they are amenable to finite model checking. The model checker finds all possible system behaviours up to some number of execution steps and examines them for violations of desired invariance properties such as safety and liveness.
The objective of the talk is to demonstrate how TLA+ can be used to eliminate design flaws before system implementation is underway.