TLA+ case study: a resource allocator

Stephan Merz

Abstract

This note presents a case study for the specification and analysis of reactive systems in TLA+. It illustrates available verification techniques and describes some pitfalls to avoid when writing formal models. It is mainly intended as a tutorial to the TLA+ language and tools and was initially developed during a Summer School in Slovakia in June 2004.

Technical report, LORIA, August 2004

Available as: [ PDF | ZIP archive with PDF and TLA+ models ]