[This blog was originally published at http://blogs.msdn.com/research]

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.

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:

“Systems are real, and behaviors of the system is a sequence of states where a state is an assignment of values to a variable”

Basic principles are found here: http://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:

• http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html

Free eBook on Specifying Systems:

• Introduction to free ebook: http://research.microsoft.com/en-us/um/people/lamport/tla/book.html#download
• Book direct download: http://research.microsoft.com/en-us/um/people/lamport/tla/book.html
• Supporting material: http://research.microsoft.com/en-us/um/people/lamport/tla/web.zip

Wildfire Verification Challenge Problem:

• The Wildfire Verification Challenge Problem