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.
Type de document :
Communication dans un congrès
Dirk Beyer; Michele Boreale. 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. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.5-19, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_2〉
https://hal.inria.fr/hal-01515239
Contributeur : Hal Ifip
<>
Soumis le : jeudi 27 avril 2017 - 10:46:45
Dernière modification le : jeudi 27 avril 2017 - 14:43:59
Document(s) archivé(s) le : vendredi 28 juillet 2017 - 12:39:26
Martín Abadi, Frank Mcsherry, Derek Murray, Thomas Rodeheffer. Formal Analysis of a Distributed Algorithm for Tracking Progress. Dirk Beyer; Michele Boreale. 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. Springer, Lecture Notes in Computer Science, LNCS-7892, pp.5-19, 2013, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-38592-6_2〉. 〈hal-01515239〉
