THIS REPORT HAS BEEN WITHDRAWN

Ankush Desai, David Broman, John Eidson, Shaz Qadeer and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2014-136
June 30, 2014

Time synchronization plays a central role in the design of reliable distributed embedded systems. However, the clocks of nodes that are time-synchronized are only guaranteed to be equal within a certain tolerance. Thus, when modeling and verifying distributed protocols that involve or rely upon time synchronization, abstractions are needed that accurately capture the notion of systems being “almost synchronized.” In this paper, we present the concept of approximate synchrony, a modeling and verification abstraction for time-synchronized systems. Approximate synchrony is a sound and tunable abstraction. We have implemented approximate synchrony as a part of a model checker and used it to verify the Best Master Clock (BMC) algorithm, the core component of IEEE 1588 precision time protocol and the time-synchronized channel hopping protocol that is part of the IEEE 802.15.4e standard.

Author Comments: Old tech report and would like to remove it.