Approximate Synchrony: An Abstraction for Distributed Time-Synchronized Systems

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

http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-136.pdf

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.


BibTeX citation:

@techreport{Desai:EECS-2014-136,
    Author = {Desai, Ankush and Broman, David and Eidson, John and Qadeer, Shaz and Seshia, Sanjit A.},
    Title = {Approximate Synchrony: An Abstraction for Distributed Time-Synchronized Systems},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2014},
    Month = {Jun},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-136.html},
    Number = {UCB/EECS-2014-136},
    Abstract = {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.}
}

EndNote citation:

%0 Report
%A Desai, Ankush
%A Broman, David
%A Eidson, John
%A Qadeer, Shaz
%A Seshia, Sanjit A.
%T Approximate Synchrony: An Abstraction for Distributed Time-Synchronized Systems
%I EECS Department, University of California, Berkeley
%D 2014
%8 June 30
%@ UCB/EECS-2014-136
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-136.html
%F Desai:EECS-2014-136