Free eBook about TLA which either it means Three Letter Acronyms or Temporal Logic of Actions
[This blog was originally published at https://blogs.msdn.com/[research](../research/sensor-touch-fun-in-reaching-out)\]
This will be the big hit, maybe bigger than the Oscar’s! In the case of this blog TLA is an acronym for the Temporal Logic of Actions, which has nothing to do with Dr. Who. Or the noise that is my style of blogging, says the man who’s name can not be said out loud.
As we get more into cloud architecture design, the better we will need to do system modeling. Now with respect to the Oscars, movies are made with a detailed eye to scripts which includes material, action and outcomes. Too often software systems are just a bunch of code put together that works, at least for the moment. But breaks easily in the future or can’t be scalable.
In the case of TLA, this is away to get into the logic of verification and to become an expert.
Temporal Logic of Actions is a way to specify systems, and with systems like Windows On Arm, this becomes much more interesting. Why? How because I say so? Not enough, oh. Ok, let’s say this:
“A specication is a blueprint of a system"
Quote from personal conversation with Leslie Lamport, Microsoft Research
Link to a book in process by Leslie Lamport:
Links to TLA+ modeling:
- Basic principles are found here: https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1994-001.pdf , and that is where the quote from above came from.
- So get started with this shiny object, start here:
Free eBook on Specifying Systems:
- Introduction to free ebook: https://research.microsoft.com/en-us/um/people/lamport/tla/book.html#download
- Book direct download: https://research.microsoft.com/en-us/um/people/lamport/tla/book.html
- Supporting material: https://research.microsoft.com/en-us/um/people/lamport/tla/web.zip
Wildfire Verification Challenge Problem: