The final publication is available via <a href="https://doi.org/10.1007/978-3-319-52234-0_19" target="_blank">https://doi.org/10.1007/978-3-319-52234-0_19</a>.
-
dc.description.abstract
Fault-tolerant distributed algorithms are a vital part of mission-critical distributed systems. In principle, automatic verification can be used to ensure the absence of bugs in such algorithms. In practice however, model checking tools will only establish the correctness of distributed algorithms if message passing is encoded efficiently. In this paper, we consider abstractions suitable for many fault-tolerant distributed algorithms that count messages for comparison against thresholds, e.g., the size of a majority of processes. Our experience shows that storing only the numbers of sent and received messages in the global state is more efficient than explicitly modeling message buffers or sets of messages. Storing only the numbers is called message-counting abstraction. Intuitively, this abstraction should maintain all necessary information. In this paper, we confirm this intuition for asynchronous systems by showing that the abstract system is bisimilar to the concrete system. Surprisingly, if there are real-time constraints on message delivery (as assumed in fault-tolerant clock synchronization algorithms), then there exist neither timed bisimulation, nor time-abstracting bisimulation. Still, we prove this abstraction useful for model checking: it preserves ATCTL properties, as the abstract and the concrete models simulate each other.
de
dc.description.sponsorship
Austrian Science Funds (FWF)
-
dc.description.sponsorship
Vienna Science and Technology Fund (WWTF)
-
dc.language
English
-
dc.language.iso
en
-
dc.publisher
Springer Heidelberg
-
dc.relation.ispartofseries
LNCS
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.title
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.relation.publication
VMCAI
-
dc.relation.grantno
S11403
-
dc.relation.grantno
S11405
-
dc.relation.grantno
ICT15-103
-
dc.rights.holder
Springer International Publishing AG 2017
-
dc.type.category
Full-Paper Contribution
-
tuw.container.volume
10145
-
tuw.version
am
-
tuw.publication.orgunit
E184 - Institut für Informationssysteme
-
tuw.publication.orgunit
E183 - Institut für Rechnergestützte Automation
-
tuw.publisher.doi
10.1007/978-3-319-52234-0_19
-
dc.identifier.libraryid
AC11361660
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:3-2936
-
tuw.author.orcid
0000-0002-9426-6314
-
tuw.author.orcid
0000-0003-2795-611X
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
open
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems