[marco_salvatori]

One can also download the TLA+ book and the TLA+ hyperbook from Leslie Lamport' TLA home page

https://lamport.azurewebsites.net/tla/tla.html

Both are very useful resources and for those interested in learning I would recommend going through both together letting the book fill in the detail where the hyperbook leaves you wanting more information. The hyperbook concetrates on PlusCal, which is a higher level interface to the TLA language, while the TLA book is all in the TLA language itself. I find,in practice,that the TLA language is what I am more comfortable writing specifications in. I find it clearer and as essentially standard mathematical notation its one less thing to learn. I believe Leslie encourages engineers to use PlusCal as being more user friendly.

Once one has worked though the specification course in the hyperbook, one should be able to apply TLA to real problems in any event driven system. (Sequential problems can also be modeled though). The primary hurdle in getting to applications will probably be coming to the understanding that modeling work happens at a much higher level of abstraction than programming, and that ones insticts as programmers, to get into detail, are not correct.

The benefits are two fold. Modeling a system before it's built forces one to abstract, clarify and simplify ones approach. The second benefit is that the model checker will find all the corner cases and complexity that one missed in the design. If one does a good translation from the model to code from there, then to a first approximation the code is bug free. As a bonus, later, when one goes back to code that has a spec, the spec is a nice summary of what has been coded (becase you forgot) and one can modify, and verify the spec before one updates the code.