Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems

Ankush Desai, Sanjit A. Seshia, Shaz Qadeer, David Broman, and John C. Eidson. Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems. In Proceedings of the 27th International Conference on Computer-Aided Verification (CAV), pp. 429–448, July 2015.
Extended tech report version available here.

Download

[pdf] 

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 should accurately capture these imperfections that cause the system to only be "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

@inproceedings{desai-cav15,
  author    = {Ankush Desai and Sanjit A. Seshia and Shaz Qadeer and David Broman and John C. Eidson},
  title     = {Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems},
 booktitle = {Proceedings of the 27th International Conference on Computer-Aided Verification (CAV)},
 month = "July",
 year = {2015},
 pages = "429--448",
 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 should accurately capture these imperfections that cause 
the system to only be "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.},
  wwwnote = {Extended tech report version available <a href="http://www.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-158.html">here</a>.} 
}

Generated by bib2html.pl (written by Patrick Riley ) on Sun May 01, 2016 00:40:09