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

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.

paper.pdf
PDF file

Publisher  Microsoft Technical Report
Copyright (c) 2013 Microsoft Corporation.

Details

TypeTechReport
NumberMSR-TR-2013-20
> Publications > The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof