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
Type de document :
Rapport
[Intern report] A04-R-101 || merz04a, 2004, 20 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00107809
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:10:25
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 12:30:33

Identifiants

  • HAL Id : inria-00107809, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

150

Téléchargements de fichiers

98