An introduction to TLA+
Echidna (Gegair) | Tue 16 Apr 10:45 a.m.–11:30 a.m.
Presented by
-
Clinton is an Open Source software engineer, who has spent most of his career supporting researchers in a wide variety of fields. At the moment they are at the Australian Synchrotron. Clinton has had an interest in formal methods since introduced to them at university.
Abstract
TLA+ is an implementation of Temporal Logic of Actions, a specification language rooted in mathematical logic, allowing specifications to be manipulated and checked by mathematical tools. TLA+ can be used to design and document specifications in an unambiguous way, and then the tooling around TLA+ can help prove that a system that implements the specification can never go into an unknown state, can't deadlock or livelock.
Open Source tends to be a source-first culture, TLA+ offers a way of verifying the specification before even starting coding. This year, the Linux Foundation formed the TLA+ foundation to form an Open foundation around TLA+ to foster development and use, so it seems like a good time to introduce the language, and the tooling around it.
Attendees should come away with a basic understanding of where TLA+ might be useful in their engineering culture.
TLA+ is an implementation of Temporal Logic of Actions, a specification language rooted in mathematical logic, allowing specifications to be manipulated and checked by mathematical tools. TLA+ can be used to design and document specifications in an unambiguous way, and then the tooling around TLA+ can help prove that a system that implements the specification can never go into an unknown state, can't deadlock or livelock. Open Source tends to be a source-first culture, TLA+ offers a way of verifying the specification before even starting coding. This year, the Linux Foundation formed the TLA+ foundation to form an Open foundation around TLA+ to foster development and use, so it seems like a good time to introduce the language, and the tooling around it. Attendees should come away with a basic understanding of where TLA+ might be useful in their engineering culture.