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

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2015-158

May 29, 2015

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-158.pdf

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, and there are transient phases while synchronization is still being achieved. Abstractions used for modeling and verification of such systems %distributed systems that involve time synchronization should accurately capture these imperfections that cause the system to only be %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 models of 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.

---

BibTeX citation:

@techreport{Desai:EECS-2015-158,
    Author= {Desai, Ankush and Seshia, Sanjit A. and Qadeer, Shaz and Broman, David and Eidson, John},
    Title= {Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems},
    Year= {2015},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-158.html},
    Number= {UCB/EECS-2015-158},
    Abstract= {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, and there are transient phases while 
synchronization is still being achieved. Abstractions used for modeling
and verification of such systems
%distributed systems that involve time synchronization 
should accurately capture these imperfections that cause the system to only be 
%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 models of 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.},
}

EndNote citation:

%0 Report
%A Desai, Ankush 
%A Seshia, Sanjit A. 
%A Qadeer, Shaz 
%A Broman, David 
%A Eidson, John 
%T Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems
%I EECS Department, University of California, Berkeley
%D 2015
%8 May 29
%@ UCB/EECS-2015-158
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-158.html
%F Desai:EECS-2015-158