Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

摘要: Fault-tolerant distributed algorithms are a vital part of mission-critical systems. In principle, automatic verification can be used to ensure the absence bugs in such algorithms. practice however, model checking tools will only establish correctness if message passing is encoded efficiently. this paper, we consider abstractions suitable for many fault-tolerant that count messages comparison against thresholds, e.g., size majority processes. Our experience shows storing numbers sent and received global state more efficient than explicitly modeling buffers or sets messages. Storing called message-counting abstraction. Intuitively, abstraction should maintain all necessary information. confirm intuition asynchronous systems by showing abstract system bisimilar concrete system. Surprisingly, there real-time constraints on delivery (as assumed clock synchronization algorithms), then exist neither timed bisimulation, nor time-abstracting bisimulation. Still, prove useful checking: it preserves ATCTL properties, as models simulate each other.