Jeff Weiss
Knows more about SCADA protocols than he cares to, Senior Software Engineer @ Enbala Power Networks
Jeff is an experienced software engineer and leader who has worked on a number of critical projects from electrical grid infrastructure, autonomous vehicles, configuration management software, and national weapons programs.
When he's not learning something new and challenging, you can find him crafting puns and dad jokes/groan-ups.
Jeff splits his time between Portland, Oregon and Düsseldorf, Germany.
Past Activities
Code BEAM STO V
16.25 - 16.50
A Beginner's Guide to TLA+: Exploring State Machines & Proving Correctness
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.