TLA+ case study: a resource allocator

Stephan Merz
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 ]

Stephan Merz
Last modified: Wed Aug 18 09:53:05 CEST 2004