Approximate Synchrony: An Abstraction for Distributed Time-Synchronized Systems
Ankush Desai

Citation
Ankush Desai. "Approximate Synchrony: An Abstraction for Distributed Time-Synchronized Systems". Tutorial, 11, September, 2014.

Abstract
Time synchronization plays a central role in the design of reliable distributed embedded systems. However, the clocks of nodes that are time-synchronized are only guaranteed to be equal within a certain tolerance. Thus, when modeling and verifying distributed protocols that involve or rely upon time synchronization, abstractions are needed that accurately capture the notion of systems being "almost synchronized." We present the concept of approximate synchrony, a modeling and verification abstraction for time-synchronized systems. Approximate synchrony is a sound and tunable abstraction. We have implemented approximate synchrony as a part of a model checker and used it to verify the Best Master Clock (BMC) algorithm, the core component of IEEE 1588 precision time protocol and the time-synchronized channel hopping protocol that is part of the IEEE 802.15.4e standard. This work is joint with John Eidson, Shaz Qadeer, David Broman, and Sanjit Seshia.

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. <a
  href="http://www.terraswarm.org/pubs/249.html"
  ><i>Approximate Synchrony: An Abstraction for
  Distributed Time-Synchronized Systems</i></a>,
  Tutorial,  11, September, 2014.

• Plain text

  Ankush Desai. "Approximate Synchrony: An Abstraction
  for Distributed Time-Synchronized Systems". Tutorial, 
  11, September, 2014.

• BibTeX

  @tutorial{Desai14_ApproximateSynchronyAbstractionForDistributedTimeSynchronized,
      author = {Ankush Desai},
      title = {Approximate Synchrony: An Abstraction for
                Distributed Time-Synchronized Systems},
      day = {11},
      month = {September},
      year = {2014},
      abstract = {Time synchronization plays a central role in the
                design of reliable distributed embedded systems.
                However, the clocks of nodes that are
                time-synchronized are only guaranteed to be equal
                within a certain tolerance. Thus, when modeling
                and verifying distributed protocols that involve
                or rely upon time synchronization, abstractions
                are needed that accurately capture the notion of
                systems being "almost synchronized." We present
                the concept of approximate synchrony, a modeling
                and verification abstraction for time-synchronized
                systems. Approximate synchrony is a sound and
                tunable abstraction. We have implemented
                approximate synchrony as a part of a model checker
                and used it to verify the Best Master Clock (BMC)
                algorithm, the core component of IEEE 1588
                precision time protocol and the time-synchronized
                channel hopping protocol that is part of the IEEE
                802.15.4e standard. This work is joint with John
                Eidson, Shaz Qadeer, David Broman, and Sanjit
                Seshia.},
      URL = {http://terraswarm.org/pubs/249.html}
  }
  

Posted by Barb Hoversten on 29 Jan 2014.
Groups: tools