Home
The subject matter and final goal for my semester project is the formal specification of a consensus protocol with TLA+.
A formal specification is a mathematical description of a system.
There are many reasons for creating a formal specification for a system. The number one goal is to identify and prevent errors in a system. These errors would not be apparent otherwise.
Distributed systems can get very complicated. It can be difficult to understand all the behaviors. Formal specification and verification are tools that can help us to find errors and to avoid them in the first place.
TLA stands for Temporal Logic of Actions. It is a mathematical logic for describing the behavior of systems. Leslie Lamport has extended work done by Amir Pnueli, 1996 winner of the Turing Award for bringing temporal logic to the computer science field.
TLA+ is a language for writing formal specifications. It has a syntax and semantics. Most of the language is simply mathematical notation necessary for writing formal specifications.
First you must translate your system into a mathematical model/abstraction, consisting of various modules, written in TLA+. The TLA+ Syntactic Analyzer will check your syntax and semantics. The TLC Model Checker will check your specification for logical errors. The TLC Model Checker will identify errors that would otherwise never be found by other methods. The TLaTeX typesetter will convert your modules from ASCII text to good LaTeX formatting.
It means using TLA+, which is really just math formulas, to describe a systems behaviors in order to prevent errors that can't be found with other methods.