Citation
Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, John Eidson. "Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems". 429-448, 9207, Springer, 2016; In Lecture Notes in Computer Science. Also in Proceedings of the 7th International Conference on Computer Aided Verification (CAV 2015), San Francisco, California, USA, 2015.

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.

Electronic downloads

• https://link.springer.com/chapter/10.1007%2F978-3-319-21668-3_25

• HTML

  Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, John
  Eidson. <a
  href="http://chess.eecs.berkeley.edu/pubs/1177.html"
  ><i>Approximate Synchrony:  An Abstraction for
  Distributed Almost-Synchronous Systems</i></a>,
  429-448, 9207, Springer, 2016; In <em>Lecture Notes in
  Computer Science</em>.
  
  Also in
  <em>Proceedings of the 7th International Conference on
  Computer Aided Verification (CAV 2015)</em>, San
  Francisco, California, USA, 2015.

• Plain text

  Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, John
  Eidson. "Approximate Synchrony:  An Abstraction for
  Distributed Almost-Synchronous Systems". 429-448, 9207,
  Springer, 2016; In <em>Lecture Notes in Computer
  Science</em>.
  
  Also in <em>Proceedings of the
  7th International Conference on Computer Aided Verification
  (CAV 2015)</em>, San Francisco, California, USA, 2015.

• BibTeX

  @inbook{DesaiSeshiaQadeerBromanEidson16_ApproximateSynchronyAbstractionForDistributedAlmostSynchronous,
      author = {Ankush Desai and Sanjit Seshia and Shaz Qadeer and
                David Broman and John Eidson},
      title = {Approximate Synchrony:  An Abstraction for
                Distributed Almost-Synchronous Systems},
      pages = {429-448},
      volume = {9207},
      publisher = {Springer},
      year = {2016},
      note = {In <em>Lecture Notes in Computer Science</em>.
  
                Also in <em>Proceedings of the 7th International
                Conference on Computer Aided Verification (CAV
                2015)</em>, San Francisco, California, USA, 2015.},
      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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/1177.html}
  }
  

Posted by Mary Stewart on 7 Jul 2016.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.