Abstract
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.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35533-7_26
Chapter PDF
Similar content being viewed by others
References
P. A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling Global Conditions in Parameterized System Verification. In Proc. CAV ‘89, LNCS 1633, pages 134–145, 1999.
P. A. Abdulla, K. Cerâns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS ‘86, pages 313–321, 1996.
T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinite-state Systems using Presburger Arithmetics. In Proc. CAV ‘87, LNCS 1254, pages 400–411, 1997.
M. C. Browne, E. M. Clarke, and O. Grumberg. Reasoning about Networks with Many Identical Finite State Processes. Information and Computation 81 (1): 13–31, 1989.
K.-T. Cheng and A. S. Krishnakumar. Automatic Generation of Functional Vectors Using the Extended Finite State Machine Model. ACM Transactions on Design Automation of Electronic Systems 1 (1): 57–79, 1996.
E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness. Verification of the Futurebus+ Cache Coherence Protocol. In Proc. 11th Int. Symp. on Computer Hardware Description Languages and their Applications, 1993.
E. Clarke, O. Grumberg, and S. Jha. Verifying Parameterized Networks. TOPLAS 19 (5): 726–750 (1997).
P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In Proc. POPL 78, pages 84–96, 1978.
G. Delzanno. Automated Verification of Parameterized Cache Coherence Protocols. To appear in Proc. CAV ‘00,July 2000.
G. Delzanno and A. Podelski, Constraint-based Deductive Model Checking in CLP. To appear in Software Tools for Technology Transfer.
J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS ‘89, pages. 352–359, 1999.
E. A. Emerson and K. S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems. In Proc. CAV ‘86, LNCS 1102, pages 87–98, 1996.
E. A. Emerson and K. S. Namjoshi. On Model Checking for Non-deterministic Infinite-state Systems. In Proc. LICS ‘88, pages 7080, 1998.
A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Technical Report LSV-98–4, Laboratoire Spécification et Vérification, Ecole Normale Supérieure de Cachan, April 1998.
S. M. German and A. P. Sistla. Reasoning about Systems with Many Processes. JACM 39 (3): 675–735 (1992)
S. Graf and H. Saldi. Construction of Abstract State Graphs with PVS. In Proc. CAV ‘87, LNCS 1254, pages 72–83, 1997.
J. Handy. The Cache Memory Book. Academic Press, 1993.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: a Model Checker for Hybrid Systems. In Proc. CAV ‘87, LNCS 1254, pages 460–463, 1997.
N. Halbwachs, Y-E. Proy, and P. Roumanoff. Verification of Real-time Systems using Linear Relation Analysis. Formal Methods in System Design, 11 (2): 157–185, 1997.
C. Norris-Ip and D. L. Dill. Verifying Systems with Replicated Components in Murphi. Formal Methods in System Design, 14 (3): 273–310, 1999.
D. Lesens, N. Halbwachs, and P. Raymond. Automatic Verification of Parameterized Linear Networks of Processes. In Proc. POPL ‘87, 1997.
K. L. McMillan and J. Schwalbe. Formal Verification of the Giga-max Cache Consistency Protocol. In Proc. Int. Symp. on Shared Memory Multiprocessors, pp. 242–51, 1991.
F. Pong and M. Dubois. A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems 6 (8), August 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Delzanno, G. (2000). Verification of Consistency Protocols Via Infinite-State Symbolic Model Checking. In: Bolognesi, T., Latella, D. (eds) Formal Methods for Distributed System Development. PSTV FORTE 2000 2000. IFIP — The International Federation for Information Processing, vol 55. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35533-7_11
Download citation
DOI: https://doi.org/10.1007/978-0-387-35533-7_11
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5264-9
Online ISBN: 978-0-387-35533-7
eBook Packages: Springer Book Archive