Tutorial T5: Modeling Concurrent State Machines in TLA+

J. Germán Rivera, Tesla

Abstract

Concurrent (communicating) state machines are present in many embedded software systems. Interactions between these state machines cannot be easily described in graphical form at a level of detail precise enough to check their correctness in all possible cases. State transitions in one state machine may affect transitions in another state machine and unintended races can be very hard to detect in testing and can easily escape to production. TLA+ is a discrete-math-based modeling language for specifying concurrent state machines. Its companion model checking tool (TLC) can help catch bugs in the state machine design. With model checking, all possible state transitions and races between concurrent state machines can be simulated to find concurrency bugs. This tutorial introduces the basics of TLA+ and how to use it to model concurrent state machines and to check them with TLC, to verify if they satisfy their intended correctness properties.

Duration: Half day

Level: Introductory (Basic knowledge of discrete mathematics can be helpful)

Presentation Topics

• TLA+ Overview
• Basic Notation
• Modeling simple sequential state machines with TLA+
• Modeling simple concurrent state machines with TLA+
• Specifying safety and liveness properties
• Describing complex state with discrete math structures
• Pluscal: An algorithmic modeling language on top of TLA+
• Modeling more complex concurrent state machines with Pluscal
• Running TLC to check TLA+ models with the TLA+ Vscode extension
• Resources for further learning

Reason for attending

Learning TLA+ on your own may be intimidating at first, but after attending this tutorial, attendees will be able to explore the TLA+ resources available online, with more confidence, learn from more complex TLA+ modeling examples and start creating their own models.

Presenter

J. Germán Rivera is a senior staff software engineer at Tesla, where he develops low-level embedded software for automotive system-on-chip platforms. He has 34 years of industry experience developing system-level software. He has also held software development positions at Google, NXP, Microsoft, Cisco, IBM, NetApp and HP. He holds a Master of Software Engineering degree from Carnegie Mellon University (USA) and a Bachelor's degree in Computer Science, from the University of Los Andes (Colombia). In his spare time, he writes Ada/SPARK embedded software for hobby projects, in which he also experiments with practical applications of formal methods.