Interactive Verification of Distributed Protocols Using Decidable Logic

摘要

Distributed systems are becoming more and more pervasive in our lives, making their correctness crucial. Unfortunately, distributed systems are notoriously hard to get right and verify. Due to the infinite state space (e.g., unbounded number of nodes and messages) and the complexity of the protocols used, verification of such systems is both undecidable and hard in practice. Numerous works have considered the problem of automatically verifying distributed and parameterized systems, e.g., [1,9,10,17,18,20,23,24,26,38]. Full automation is extremely appealing. Unfortunately, automatic techniques are bound to fail in some cases due to the undecidability of the problem. Some impose restrictions on the verified systems (e.g., [26]), some may diverge (e.g., [24]) and some may report false alarms (e.g., [2]). Moreover, such techniques often suffer from scalability issues and from an unpredictable performance. As a result, most efforts towards verifying real-world systems use relatively little automation [19,25,31].