A TLA+ Module for Asynchronous Message-Passing Systems
Amy House, Peiyi Tang · 2018
The combinatorial explosion of states makes distributed, asynchronous systems difficult for humans to reason about. Leslie Lamport's TLA+, a specification language based on Temporal Logic of Actions, provides a precise, formal language for discussing such systems without needing high-level mathematics. In this paper, we provide a reusable TLA+module for specifying and model checking asynchronous message-passing systems. TLA+syntax and semantics are introduced as we describe the module.