THIS REPORT HAS BEEN WITHDRAWN

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

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2015-153
May 20, 2015

Forms of synchrony can greatly simplify modeling, design, and verification of distributed systems. Thus, recent advances in clock synchronization protocols and their adoption hold promise for system design. However, these protocols synchronize the distributed clocks only within a certain tolerance. Abstractions used for modeling and verification of distributed systems that involve time synchronization, should accurately capture the notion of the system being ``almost synchronized.'' In this paper, we present approximate synchrony, a sound and tunable abstraction for verification of almost-synchronous systems. We show how approximate synchrony can be used for verification of both time synchronization protocols and applications running on top of them. We provide an algorithmic approach for constructing this abstraction for symmetric, almost-synchronous systems, a subclass of almost-synchronous systems. Moreover, we show how approximate synchrony also provides a useful strategy to guide state-space exploration. 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 the IEEE 1588 precision time protocol, as well as the time-synchronized channel hopping protocol that is part of the IEEE 802.15.4e standard.

Author Comments: We have updated this techreport and havepublished another one. We would like to withdraw this one.