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.
Book: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
Leave a reply