×

zbMATH — the first resource for mathematics

Efficient approximate verification of B and Z models via symmetry markers. (English) Zbl 1209.68127
Summary: We present a new approximate verification technique for falsifying the invariants of B models. The technique employs symmetry of B models induced by the use of deferred sets. The basic idea is to efficiently compute markers for states, so that symmetric states are guaranteed to have the same marker (but not the other way around). The falsification algorithm then assumes that two states with the same marker can be considered symmetric. We describe how symmetry markers can be efficiently computed and empirically evaluate an implementation, showing both very good performance results and a high degree of precision (i.e., very few non-symmetric states receive the same marker). We also identify a class of B models for which the technique is precise and therefore provides an efficient and complete verification method. Finally, we show that the technique can be applied to Z models as well.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68R10 Graph theory (including graph drawing) in computer science
03B70 Logic in computer science
68N17 Logic programming
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial, J.-R.: The B-Book. Cambridge University Press (1996)
[2] Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010) · Zbl 1213.68214
[3] Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: ICFEM06, LNCS 4260, pp. 588–605. Springer (2006)
[4] B-Core (UK) Ltd, Oxon, UK. B-Toolkit, On-line manual. Available at http://www.b-core.com/ONLINEDOC/Contents.html (1999). Accessed 10 August 2010
[5] Barner, S., Grumberg, O.: Combining symmetry reduction and under-approximation for symbolic model checking. Form. Methods Syst. Des. 27(1–2), 29–66 (2005) · Zbl 1085.68086 · doi:10.1007/s10703-005-2246-x
[6] Ben-Ari, M.: Principles of the Spin Model Checker. Springer (2008) · Zbl 1142.68044
[7] Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. STTT 4(1), 92–106 (2002) · Zbl 02178179 · doi:10.1007/s100090200074
[8] Bosnacki, D., Donaldson, A.F., Leuschel, M., Massart, T.: Efficient approximate verification of promela models via symmetry markers. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Proceedings ATVA 2007, LNCS 4762, pp. 300–315. Springer (2007) · Zbl 1141.68453
[9] Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1–2), 77–104 (1996) · Zbl 05475431 · doi:10.1007/BF00625969
[10] Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
[11] ClearSy, Aix-en-Provence, France. B4Free: Tool and Manuals. Available at http://www.b4free.com (2006). Accessed 10 August 2010
[12] Derrick, J., North, S., Simons, A.: Z2sal: a translation-based model checker for z. Form. Asp. Comput. doi: 10.1007/s00165-009-0126-7 · Zbl 1214.68133
[13] Derrick, J., North, S., Simons, A.J.H.: Z2SAL–building a model checker for Z. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) Proceedings ABZ 2008, LNCS 5238, pp. 280–293 (2008)
[14] Derrick, J., North, S., Simons, T.: Issues in implementing a model checker for Z. In: Liu, Z., He, J. (eds.) ICFEM, LNCS 4260, pp. 678–696. Springer (2006)
[15] Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: International Conference on Computer Design, pp. 522–525 (1992)
[16] Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) Proceedings FM 2005, LNCS 3582, pp. 481–496. Springer (2005) · Zbl 1120.68414
[17] Donaldson, A.F., Miller, A.: Exact and approximate strategies for symmetry reduction in model checking. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings FM’2006, LNCS 4085, pp. 541–556. Springer (2006)
[18] Donaldson, A.F., Miller, A., Calder, M.: Finding symmetry in models of concurrent systems by static channel diagram analysis. Electr. Notes Theor. Comput. Sci. 128(6), 161–177 (2005) · Zbl 05415159 · doi:10.1016/j.entcs.2005.04.010
[19] Donaldson, A.F., Miller, A., Calder, M.: Spin-to-grape: a tool for analysing symmetry in promela models. Electr. Notes Theor. Comput. Sci. 139(1), 3–23 (2005) · Zbl 05415160 · doi:10.1016/j.entcs.2005.09.007
[20] Emerson, E.A., Sistla, A.P.: Utilizing symmetry when model checking under fairness assumptions: an automata-theoretic approach. In: Wolper, P. (ed.) Proceedings CAV’95, LNCS 939, pp. 309–324. Springer (1995)
[21] Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des. 9(1/2), 105–131 (1996) · Zbl 05475432 · doi:10.1007/BF00625970
[22] Flannery, S.: In Code: A Mathematical Adventure. Profile Books Ltd (2001) · Zbl 1006.01014
[23] Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) Proceedings FORMATS 2003, LNCS 2791, pp. 46–59. Springer (2003) · Zbl 1099.68657
[24] Holzmann, G.J.: An improved protocol reachability analysis technique. Softw. Pract. Exp. 18(2), 137–161 (1988) · doi:10.1002/spe.4380180203
[25] Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997) · Zbl 05113845 · doi:10.1109/32.588521
[26] Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2004)
[27] Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1/2), 41–75 (1996) · Zbl 05475430 · doi:10.1007/BF00625968
[28] Jackson, D., Jha, S., Damon, C.: Isomorph-free model enumeration: A new method for checking relational specifications. ACM Trans. Program. Lang. Syst. 20(2), 302–343 (1998) · doi:10.1145/276393.276396
[29] Jha, S.: Semmetry and induction in model checking. PhD thesis, School of Computer Science, Carnegie Mellon University (1996)
[30] Kocay, W., Kreher, D.L.: Graphs, algorithms and optimization. Chapman & Hall/CRC (2004) · Zbl 1079.05001
[31] Kreher, D.L., Stinson, D.R.: Combinatorial Algorithms: Generation, Enumeration, Search. CRC Press (1999) · Zbl 0911.05002
[32] Leuschel, M.: The high road to formal validation. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) Proceedings ABZ 2008, LNCS 5238, pp. 4–23 (2008) · Zbl 1156.68473
[33] Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods, LNCS 2805, pp. 855–874. Springer (2003)
[34] Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) Proceedings ICFEM’05, LNCS 3785, pp. 345–359. Springer (2005)
[35] Leuschel, M., Butler, M., Spermann, C., Turner, E.: Symmetry reduction for B by permutation flooding. In: Proceedings B2007, LNCS 4355, pp. 79–93. Springer, Besancon, France (2007)
[36] Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2):185–203 (2008) · Zbl 05536137 · doi:10.1007/s10009-007-0063-9
[37] Leuschel, M., Massart, T.: Efficient approximate verification of B via symmetry markers. In: Proceedings International Symmetry Conference, pp. 71–85. Edinburgh, UK (2007) · Zbl 1141.68453
[38] Manku, G.S., Hojati, R., Brayton, R.K.: Structural symmetry and model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Proceedings CAV’98, LNCS 1427, pp. 159–171. Springer (1998)
[39] Matos, P.J., Fischer, B., Silva, J.P.M.: A lazy unbounded model checker for event-b. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM of Lecture Notes in Computer Science, vol. 5885, pp. 485–503. Springer (2009)
[40] McKay, B.: Nauty user’s guide. Available via http://cs.anu.edu.au/people/bdm/nauty/ . Accessed 10 August 2010
[41] McKay, B.D.: Practical graph isomorphism. Congressus Numerantium. 30, 45–87 (1981)
[42] Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3), 8 (2006) · doi:10.1145/1132960.1132962
[43] Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981) · Zbl 0474.68031 · doi:10.1016/0020-0190(81)90106-X
[44] Plagge, D., Leuschel, M.: Validating Z specificatons using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) Proceedings IFM 2007, LNCS 4591, pp. 480–500. Springer (2007)
[45] Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 11, 9–21 (2010) · Zbl 05781756 · doi:10.1007/s10009-009-0132-3
[46] Schneider, S.: The B-method, An Introduction. Computer Science–The Cornerstones of Computing Series. Palgrave, macmillan (2001)
[47] Sistla, A.P., Gyuris, V., Emerson, E.A.: Smc: a symmetry-based model checker for verification of safety and liveness properties. ACM Trans. Softw. Eng. Methodol. 9(2), 133–166 (2000) · doi:10.1145/350887.350891
[48] Spermann, C., Leuschel, M.: ProB gets nauty: effective symmetry reduction for B and Z models. In: Proceedings TASE 2008, pp. 15–22. IEEE, Nanjing, China (2008)
[49] France Steria, Aix-en-Provence: Atelier B, user and reference manuals. Available at http://www.atelierb.eu (1996). Accessed 10 August 2010
[50] Turner, E., Leuschel, M., Spermann, C., Butler, M.J.: Symmetry reduced model checking for B. In: Proceedings TASE 2007, pp. 25–34. IEEE Computer Society (2007)
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.