Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Approximate synchrony: An abstraction for distributed almost-synchronous systems
University of California, Berkeley.
University of California, Berkeley.
Microsoft Research.
KTH, School of Information and Communication Technology (ICT), Software and Computer systems, SCS. KTH Royal Institute of Technology and University of California, Berkeley. (Model-based Computing System (MCS))ORCID iD: 0000-0001-8457-4105
Show others and affiliations
2015 (English)In: Proceedings of the 27th International Conference on Computer Aided Verification, CAV 2015, Springer, 2015, 429-448 p.Conference paper, Published paper (Refereed)
Resource type
Text
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2015. 429-448 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9207
Keyword [en]
Abstracting, Clocks, Computer aided analysis, Space research, Standards, Synchronization, Algorithmic approach, Clock Synchronization, Distributed systems, Modeling and verifications, Precision time protocols, State space exploration, Synchronous system, Time synchronization protocols, Model checking
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:kth:diva-181630DOI: 10.1007/978-3-319-21668-3_25Scopus ID: 2-s2.0-84951146003ISBN: 9783319216676 (print)OAI: oai:DiVA.org:kth-181630DiVA: diva2:902447
Conference
18 July 2015 through 24 July 2015
Note

QC 20160211

Available from: 2016-02-11 Created: 2016-02-02 Last updated: 2017-01-11Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Broman, David
By organisation
Software and Computer systems, SCS
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 34 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf