Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof

Thomas L. Rodeheffer

Abstract

This report presents a formal specification, written in TLA+, for the Naiad Clock protocol, along with the results of checking the specification using the TLC model checker. Also presented is a formal proof of the Naiad Clock safety properties, which has been mechanically checked using the TLA+ proof system.

This report is based partly on work with Martin Abadi, Frank McSherry, and Derek Murray.

Details

Publication typeTechReport
NumberMSR-TR-2013-20
PublisherMicrosoft Technical Report

Newer versions

Martin Abadi, Frank McSherry, Derek G. Murray, and Thomas L. Rodeheffer. Formal Analysis of a Distributed Algorithm for Tracking Progress, Springer, 3 June 2013.

> Publications > The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof