A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness | Jeff Weiss | Code BEAM V

#Code BEAM V 2020

TALK LEVEL: BEGINNER / INTERMEDIATE / ADVANCED

This talk introduces TLA+ by taking a small package from hex, examining its properties, modeling its behaviour as a state machine, creating TLA+ correctness and liveness specifications for it, and then using the TLA+ model checker to prove correctness. No prior exposure to formal methods like TLA+ or PlusCalc are necessary. A passing familiarity with state machines is recommended, but not required.

THIS TALK IN THREE WORDS

Formal

State

Machines

OBJECTIVES

Introduce TLA+ and its value
Illustrate conversion of a state machine to a TLA+ specification
Building and checking correctness and liveness models of that TLA+ specification

TARGET AUDIENCE

Developers interested in adding more rigour to their problem solving and more quickly surfacing design errors.

Jeff Weiss

Back to all media