Auxiliary Variables in TLA+

Abstract : Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implementation without changing its semantics–that is, the set of behaviors that it describes. This paper explains rules for adding history, prophecy, and stuttering variables to TLA+ specifications, ensuring that the augmented specification is equivalent to the original one. The rules are explained with toy examples, and they are used to verify the correctness of a simplified version of a snapshot algorithm due to Afek et al.
Type de document :
Rapport
[Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France); Microsoft Research. 2017
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01488617
Contributeur : Stephan Merz <>
Soumis le : dimanche 28 mai 2017 - 14:19:04
Dernière modification le : mercredi 8 novembre 2017 - 12:08:09
Document(s) archivé(s) le : mercredi 6 septembre 2017 - 10:36:25

Fichiers

auxiliary.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01488617, version 2
  • ARXIV : 1703.05121

Collections

Citation

Leslie Lamport, Stephan Merz. Auxiliary Variables in TLA+. [Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France); Microsoft Research. 2017. 〈hal-01488617v2〉

Partager

Métriques

Consultations de la notice

85

Téléchargements de fichiers

16