Draper Clock-Synchronization Protocol in SAL

In 1973, Daly, Hpokins, and McKenna (from Draper Lab.) presented a fault-tolerant digital clocking system at the FTCS conference. This is probably one of the first published system designs that is intended to tolerate arbitrary, asymmetric faults (i.e., Byzantine faults).

The following SAL models (05/14/2012) are two variant formalizations of this Draper Clock-Synchronization Protocol developed by Ashish Tiwari.