×

zbMATH — the first resource for mathematics

Finite reasons for safety. Parameterized verification by finite model finding. (English) Zbl 1314.68185
Summary: In this paper we investigate to what extent a very simple and natural “reachability as deducibility” approach, originating in research on formal methods for security, is applicable to the automated verification of large classes of infinite state and parameterized systems. In this approach the verification of a safety property is reduced to the purely logical problem of finding a countermodel for a first-order formula. This task is delegated then to generic automated finite model building procedures. A finite countermodel, if found, provides with a concise representation for a system invariant sufficient to establish the safety. In this paper we first present a detailed case study on the verification of a parameterized mutual exclusion protocol. Further we establish the relative completeness of the finite countermodel finding method (FCM) for a class of parameterized linear arrays of finite automata with respect to known methods based on monotonic abstraction and symbolic backward reachability. The practical efficiency of the method is illustrated on a set of verification problems taken from the literature using Mace4 model finding procedure.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
E-Darvin; Mace4; Mcmt; Prover9
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, PA; Jonsson, B, Verifying programs with unreliable channels, Inf. Comput., 127, 91-101, (1996) · Zbl 0856.68096
[2] Abdulla, PA; Delzanno, G; Henda, NB; Rezine, A, Monotonic abstraction: on efficient verification of parameterized systems, Int. J. Found. Comput. Sci., 20, 779-801, (2009) · Zbl 1186.68272
[3] Abdulla, PA; Delzanno, G; Rezine, A, Approximated context-sensitive analysis for parameterized verification, Lect. Notes Comput. Sci., 5522, 41-56, (2009)
[4] Baumgartner, P; Pelzer, B; Tinelli, C, Model evolution with equality—revised and implemented, J. Symb. Comput., 47, 1011-1045, (2012) · Zbl 1258.03020
[5] Caferra, R., Leitsch, A., Peltier, M.: Automated model building. In: Applied Logic Series, vol. 31. Kluwer (2004) · Zbl 1085.03009
[6] Comon, H.: Inductionless induction. In: David, R. (ed.) 2nd Int. Conf. in Logic for Computer Science: Automated Deduction. Lecture Notes. Uni de Savoie, Chambery (1994) · Zbl 0994.03006
[7] Delzanno, G, Constraint-based verification of parametrized cache coherence protocols, Formal Methods Syst. Des., 23, 257-301, (2003) · Zbl 1073.68518
[8] Enderton, H.: A Mathematical Introduction to Logic. Academic Press (1972) · Zbl 0298.02002
[9] Fisman, D., Pnueli, A.: Beyond regular model checking. In: Proc. of FSTTCS’01. LNCS, vol. 2245 (2001) · Zbl 1052.68084
[10] Ghilardi, S; Ranise, S; MCMT, A model checker modulo theories, Lect. Notes Comput. Sci., 6173, 22-29, (2010) · Zbl 1291.68257
[11] Ghilardi, S., Nikolini, E., Ranise, S., Zucchelli, D.: Towards SMT model-checking of array-based systems. In: IJCAR, LNCS (2008) · Zbl 1165.68406
[12] Goubault-Larrecq, J.: Towards producing formally checkable security proofs, automatically. In: Computer Security Foundations (CSF), pp. 224-238 (2008) · Zbl 1186.68272
[13] Goubault-Larrecq, J, Finite models for formal security proofs, J. Comput. Secur., 18, 1247-1299, (2010)
[14] Guttman, J.: Security theorems via model theory. In: Proceedings 16th International Workshop on Expressiveness in Concurrency, EXPRESS, EPTCS, vol. 8 (2009)
[15] Habermehl, P; Vojnar, T, Regular model checking using inference of regular languages, Electron. Notes Theor. Comput. Sci. (ENTCS), 138, 21-36, (2005) · Zbl 1272.68256
[16] Jurjens, J., Weber, T.: Finite models in FOL-based crypto-protocol verification. In: Degano, P., Viganò, L. (eds.) ARSPA-WITS 2009, LNCS 5511, pp. 155-172 (2009) · Zbl 1252.94078
[17] Kapur, D; Musser, DR, Proof by consistency, Artif. Intell., 31, 125-157, (1987) · Zbl 0631.68073
[18] Lallement, G.: Semigroups and Combinatorial Applications. Wiley (1979)
[19] Lisitsa, A.: Verfication via countermodel finding. http://www.csc.liv.ac.uk/ alexei/countermodel
[20] Lisitsa, A.: Reachability as deducibility, finite countermodels and verification. In: Preproceedings of AVOCS 2009, Technical Report of Computer Science, Swansea University, CSR-2-2009, pp. 241-243 (2009)
[21] Lisitsa, A.: Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol. In: Proceedings of WING 2010, 1 pp. (2010)
[22] Lisitsa, A.: Reachability as deducibility, finite countermodels and verification. In: Proceedings of ATVA 2010. LNCS, vol. 6252, pp. 233-244 (2010) · Zbl 1305.68119
[23] Lisitsa, A.: Finite model finding for parameterized verification. CoRR arXiv:1011.0047 (2010). Accessed 12 Feb 2013 · Zbl 1305.68119
[24] Lisitsa, A.: Finite countermodels for safety verification of parameterized tree systems. CoRR arXiv:1107.5142. Accessed 12 Feb 2013
[25] Lisitsa, A.: Finite models vs tree automata in safety verification. In: 23rd International Conference on Rewriting Techniques and Applications RTA’12, pp. 225-239 (2012) · Zbl 1268.03036
[26] McCune, W.: Prover9 and Mace4. http://www.cs.unm.edu/ mccune/mace4. Accessed 12 Feb 2013
[27] Nilsson, M.: Regular model checking. Acta Universitatis Upsaliensis. Uppsala Dissertations from the Faculty of Science and Technology 60. 149 pp. Uppsala. ISBN 91-554-6137-9 (2005)
[28] Nonnengart, A.: Hybrid systems verification by location elimination. In: Lynch, N.A., Krogh, B.H. (eds.) Hybrid Systems: Computation and Control, Third International Workshop, HSCC 2000, LNCS, vol. 1790, pp. 352-365 (2000) · Zbl 0938.93554
[29] Selinger, P, Models for an adversary-centric protocol logic, Electron. Notes Theor. Comput. Sci., 55, 69-84, (2001) · Zbl 1268.03036
[30] Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.): CADE-16, LNAI, vol. 1632, pp. 314-328 (1999) · Zbl 1038.94548
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.