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

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

Рет қаралды 6,939

Күн бұрын

This video was recorded at Code BEAM V 2020 - codesync.global/conferences/code-beam-sto/
A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness | Jeff Weiss - Senior Software Engineer at Enbala Power Networks
ABSTRACT
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.
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.
• Follow us on social:
Twitter: / codebeamio
LinkedIn: / 27159258
• Looking for a unique learning experience?
Attend the next Code Sync conference near you!
See what's coming up at: codesync.global
• SUBSCRIBE TO OUR CHANNEL
/ @codesync

Пікірлер: 5

@nirmalyasengupta2332 2 жыл бұрын

Concise presentation, thanks! I have been tinkering with TLA+ for a few months now (I am still a novice). It takes me some time before I get my head around the syntax and symbols, but it forces me to think about the decisions behind a design and the consequences of the same, *more clearly*. I have had the opportunity to build a number of production-level components using Finite State Machine-based approaches (all handcrafted, no tools) and I am quite a fan of FSM-driven design. However, I think that in TLA+, being able to add __temporal__ aspect to properties helps matters a lot. Breakage in transitions are found much more readily. It will be good to hear from you about your experience, of using TLA+ for a production-level component and the benefits you have derived from the adoption of TLA+.

@marshallross3373 2 жыл бұрын

Ya, great demo. Thanks for posting!

@TheRedbeardster 2 жыл бұрын

Very nice!

@lelev760 2 жыл бұрын

Hi, would you be able to share a link to the tla+ model code you showed? I'd be interested in running it. I've been tinkering with tla+. Thanks

@bayareacarnatic 3 ай бұрын

I tried to take the above example and try it out the tla+ tool but it never allows me to add VALUES. People have thrown tonne of random materials with out a decent explanation on how to get started and use the syntax.