@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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 here.}
}