Book: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

A gentle introduction to specifying concurrent systems with the Temporal Logic of Actions, and the use of the TLC model checker to test them out.