This course will introduce necessary theoretical background.
No strong math or logic or programming knowledge is required.
Abstract:
TLA+ is a formal specification language invented by Leslie Lamport, ACM Turing
award winner. Amazon Web Service is expanding the database team using TLA+ as the formal
method tools in their key projects, such as DynamoDB. This course introduces the
fundamental knowledge of TLA+ in an incremental way by exempels of specification.
Moreover, it illustrates the methodology of formal verification using TLA+.
Part I: Fundamentals of TLA+
24.10. Motivation and Introduction
Tutorial: Introduction of TLA+ tools
31.10. Arithmetic and Algebra: Sets, functions, transition system
Tutorial: Transition system modeling
07.11. Logics: propositional logics, first-order logic
Tutorial: Exercises of logic inferences
14.11. Specifying a simple clock
Tutorial: Introduction of TLA+ specification language
21.11. Specifying the simple clock in PlusCal
Tutorial: Introduction of the pseudo code language PlusCal
28.11. Introduction of TLC: a Model Checker for TLA+
Tutorial: Using TLC model checker to check the simple clock
05.12. Specifying an asynchronous interface
Tutorial: Types, definitions and comments
12.12. Specifying a caching memory
Tutorial: Functions and tuples
19.12. Summary of TLA+ syntax and semantics
Tutorial: Some more mathematics and logic
Part II: Formal verification using TLA+
09.01. The Euclid’s Algorithm
Tutorial: Translation of pluscal specification in TLA+
Assignment pool:
a) 20 logic math; 1 point
b) 10 formula semantics; 2 points
c) 10 question answering of TLA+,
TLC, TLAPS, PlusCal; 1 point
d) 5 modeling challenges; 4 points
e) 2 small proof challenges; 5 points
f) 10 open questions; 1 point |
