VERIFICATION OF CONSISTENCY PROTOCOLS VIA INFINITE-STATE SYMBOLIC MODEL CHECKING A Case Study: the IEEE Futurebus+ Protocol
Giorgio Delzanno · 2000
We apply infinite-state model checking to verify safety properties of a pammeterized formulation of the IEEE Futurebus+ coherence proto col 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 param eterized 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 pa rameterized version of the Futurebus+ protocol has been automatically verified.