Verification of Consistency Protocols Via Infinite-State Symbolic Model Checking

We apply infinite-state model checking to verify safety properties of a parameterized formulation of the IEEE Futurebus+ coherence protocol modeled at the behavior level in a system with split transaction. This case-study shows that verification techniques previously applied to hybrid and real-time systems can be used as tools for validating parameterized protocols. This technology transfer is achieved by combining abstraction techniques, symbolic representation via constraints, efficient operations based on real arithmetics, and reachability algorithms. To our knowledge this is the first time that safety properties for a parameterized version of the Futurebus+ protocol has been automatically verified.