Auxiliary Variables in TLA+ - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2017

Auxiliary Variables in TLA+

(1) , (2, 3)
1
2
3

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.
Fichier principal
Vignette du fichier
auxiliary.pdf (487.85 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01488617 , version 1 (13-03-2017)
hal-01488617 , version 2 (28-05-2017)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More