HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

TLA+ Case Study: A Resource Allocator

Stephan Merz 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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. || Ce rapport expose une étude de cas concernant les spécification et analyse d'un système réactif en TLA+. Il présente les techniques de vérification associées à TLA+ et décrit quelques pièges à éviter lors de la rédaction de modèles formels. Son objectif p
Document type :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2006 - 9:10:25 AM
Last modification on : Friday, February 4, 2022 - 3:31:22 AM
Long-term archiving on: : Friday, November 25, 2016 - 12:30:33 PM


  • HAL Id : inria-00107809, version 1



Stephan Merz. TLA+ Case Study: A Resource Allocator. [Intern report] A04-R-101 || merz04a, 2004, 20 p. ⟨inria-00107809⟩



Record views


Files downloads