mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
An UPPAAL Model for Formal Verification of Master/Slave Clock
Universitat de les Illes Balears, Spain.ORCID iD: 0000-0002-4987-7669
Mälardalen University, Department of Computer Science and Electronics.ORCID iD: 0000-0002-7235-6888
2006 (English)In: Factory Communication Systems, 2006 IEEE International Workshop on, 2006, p. 3-12Conference paper, Published paper (Refereed)
Abstract [en]

Many distributed applications require a clock synchronization service. We have previously proposed a clock synchronization service for the Controller Area Network (CAN), which we have claimed to provide highly synchronized clocks even in the occurrence of faults in the system. In this paper we substantiate this claim by providing a formal model and verification of our fault tolerant clock synchronization mechanism. We base our modeling and verification on timed automata theory as implemented by the model checking tool UPPAAL. In the modeling we introduce a novel technique for modeling drifting clocks. The verification shows that a precision in the order of 2 μs is guaranteed despite node’s faults as well as consistent channel faults. It also shows that inconsistent channel faults may significantly worsen the achievable precision, but that this effect can be reduced by choosing a suitable resynchronization period.

Place, publisher, year, edition, pages
2006. p. 3-12
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-6904DOI: 10.1109/WFCS.2006.1704117ISBN: 1-4244-0379-0 (print)OAI: oai:DiVA.org:mdh-6904DiVA, id: diva2:236914
Conference
IEEE International Workshop on Factory Communication Systems Desc:Proceedings of a meeting held 27-30 June 2006, Torino, Italy.
Available from: 2009-09-25 Created: 2009-09-25 Last updated: 2015-07-31Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Rodriguez-Navas, GuillermoHansson, Hans

Search in DiVA

By author/editor
Rodriguez-Navas, GuillermoHansson, Hans
By organisation
Department of Computer Science and Electronics
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 27 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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