| The PDF https://github.com/rodgarrison/tla_note1/blob/main/doc/tla.p... will do much better. TLA is an acronym for Temporal Logic of Actions originally written by L. Lamport of PAXOS fame. The PDF contains numerous links to videos, books, docs, because TLA is widely supported and used. TLA is like SPIN (http://spinroot.com/spin/whatispin.html) another well known model checker based on Promula not TLA syntax. And these tools fit into a larger universe of formal verification including, for example, COQ, Isabelle, Verdi, Dafny. The purpose of these tools (indeed they are all toolsets) is to: - allow one to precisely state what safety and liveness properties a system should have. Sometimes we don't even know what those conditions are until we sit down and try typing it up. - find counter examples to those safety, liveness conditions e.g. does my buffer overflow? did I deadlock? is one of my threads waiting forever? did my account balance ever go wrong? where? why? People like these tools esp. for concurrent and distributed work where the program paths, call sequences is highly exponential and highly combinatorial and where one wants some assurance all the threads really work and get to the right post conditions and system behaviors. |