Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems
Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, Eidson John

Citation
Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, Eidson John. "Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems". 27th International Conference on Computer Aided Verification, 429-448, 18, July, 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


Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.
Citation formats  
  • HTML
    Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman,
    Eidson John. <a
    href="http://www.terraswarm.org/pubs/577.html"
    >Approximate Synchrony: An Abstraction for Distributed
    Almost-Synchronous Systems</a>, 27th International
    Conference on Computer Aided Verification, 429-448, 18,
    July, 2015.
  • Plain text
    Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman,
    Eidson John. "Approximate Synchrony: An Abstraction for
    Distributed Almost-Synchronous Systems". 27th
    International Conference on Computer Aided Verification,
    429-448, 18, July, 2015.
  • BibTeX
    @inproceedings{DesaiSeshiaQadeerBromanJohn15_ApproximateSynchronyAbstractionForDistributedAlmostSynchronous,
        author = {Ankush Desai and Sanjit Seshia and Shaz Qadeer and
                  David Broman and Eidson John},
        title = {Approximate Synchrony: An Abstraction for
                  Distributed Almost-Synchronous Systems},
        booktitle = {27th International Conference on Computer Aided
                  Verification},
        pages = {429-448},
        day = {18},
        month = {July},
        year = {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://terraswarm.org/pubs/577.html}
    }
    

Posted by Barb Hoversten on 29 May 2015.
Groups: tools

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.