Abstract
The technique of counterexample-guided abstraction refinement (Cegar) has been successfully applied in the areas of software and hardware verification. Automatic abstraction refinement is also desirable for the safety verification of complex infinite-state models. This paper investigates Cegar in the context of formal models of network protocols, in our case, the verification of fifo systems. Our main contribution is the introduction of extrapolation-based path invariants for abstraction refinement. We develop a range of algorithms that are based on this novel theoretical notion, and which are parametrized by different extrapolation operators. These are utilized as subroutines in the refinement step of our Cegar semi-algorithm that is based on recognizable partition abstractions. We give sufficient conditions for the termination of Cegar by constraining the extrapolation operator. Our empirical evaluation confirms the benefit of extrapolation-based path invariants.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Jonsson, B.: Verifying Programs with Unreliable Channels. Information and Computation 127(2), 91–101 (1996)
Berstel, J.: Transductions and Context-Free Languages. Teubner (1979)
Boigelot, B., Godefroid, P.: Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs. Formal Methods in System Design 14(3), 237–255 (1999)
Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The Power of QDDs. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 172–186. Springer, Heidelberg (1997)
Bouajjani, A., Habermehl, P.: Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations. Theoretical Computer Science 221(1-2), 211–250 (1999)
Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)
Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Brand, D., Zafiropulo, P.: On Communicating Finite-State Machines. Journal of the ACM 30(2), 323–342 (1983)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM 50(5), 752–794 (2003)
Finkel, A., Iyer, S.P., Sutre, G.: Well-Abstracted Transition Systems: Application to FIFO Automata. Information and Computation 181(1), 1–31 (2003)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proc. Symposium on Principles of Programming Languages 2002, pp. 58–70. ACM Press, New York (2002)
Jard, C., Raynal, M.: De la Nécessité de Spécifier des Propriétés pour la Vérification des Algorithmes Distribués. Rapports de Recherche 590, IRISA Rennes (December 1986)
Liège Automata-based Symbolic Handler (Lash). Tool Homepage, http://www.montefiore.ulg.ac.be/~boigelot/research/lash/
Le Gall, T., Jeannet, B., Jéron, T.: Verification of Communication Protocols using Abstract Interpretation of FIFO queues. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 204–219. Springer, Heidelberg (2006)
Model Checker for Systems of Communicating Fifo Machines (McScM). Tool Homepage, http://www.labri.fr/~heussner/mcscm/
Tools and Libraries for Static Analysis and Verification. Tool Homepage, http://gforge.inria.fr/projects/bjeannet/
Tool for Reachability Analysis of CompleX Systems (Trex). Tool Homepage, http://www.liafa.jussieu.fr/~sighirea/trex/
Yu, F., Bultan, T., Cova, M., Ibarra, O.H.: Symbolic String Verification: An Automata-Based Approach. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 306–324. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heußner, A., Le Gall, T., Sutre, G. (2009). Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems. In: Păsăreanu, C.S. (eds) Model Checking Software. SPIN 2009. Lecture Notes in Computer Science, vol 5578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02652-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-02652-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02651-5
Online ISBN: 978-3-642-02652-2
eBook Packages: Computer ScienceComputer Science (R0)