Abstract : Tracking the progress of computations can be both important and
delicate in distributed systems. In a recent distributed algorithm
for this purpose, each processor maintains a delayed view of the
pending work, which is represented in terms of points in virtual
time. This paper presents a formal specification of that algorithm
in the temporal logic TLA, and describes a mechanically verified
correctness proof of its main properties.
https://hal.inria.fr/hal-01515239
Contributor : Hal Ifip
<>
Submitted on : Thursday, April 27, 2017 - 10:46:45 AM
Last modification on : Thursday, April 27, 2017 - 2:43:59 PM
Document(s) archivé(s) le : Friday, July 28, 2017 - 12:39:26 PM
Martín Abadi, Frank Mcsherry, Derek Murray, Thomas Rodeheffer. Formal Analysis of a Distributed Algorithm for Tracking Progress. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.5-19, ⟨10.1007/978-3-642-38592-6_2⟩. ⟨hal-01515239⟩
