<

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

Jeff Weiss
Code BEAM STO V
11 Sep 2020
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.