Title: Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Language: English
Authors: Konnov, Igor V. 
Widder, Josef 
Spegni, Francesco 
Luca, Spalazzi 
Issue Date: 2017
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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-2936
Library ID: AC11361660
Organisation: E183 - Institut für Rechnergestützte Automation 
Publication Type: Inproceedings
Appears in Collections:Conference Paper

Files in this item:

Page view(s)

checked on Jul 28, 2021


checked on Jul 28, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.