Application of weaker simulations to parameterized model checking by network invariants

I. V. Konnov

Modelirovanie i analiz informacionnyh sistem, Tome 15 (2008) no. 3, pp. 3-13.

Résumé

In this paper, we consider parameterized model checking problem of asynchronously communicating processes in the framework of network invariants. The framework of network invariants exploits relations over labelled transition systems such as simulation, bisimulation, trace equivalence and trace inclusion. In the case of asynchronous parallel composition simulation and bisimulation are supposed to be rather strong and additional abstractions are required. In our work three weaker simulation relations are proposed: quasi-block simulation, block simulation and semi-block simulation. Quasi-block simulation has all the properties to be applied in the framework of network invariants. Block simulation is a stronger relation than a quasi-block simulation. It is used to find an invariant. An initial block simulation over two models exists if and only if an initial semi-block simulation over that models exists. Thus, it is sufficient to compute a semi-block simulation on the models. The sketch of an algorithm to perform such a computation is presented. Previously, we used the framework to check a parameterized model of RSVP protocol. In this paper a series of optimizations that decrease the time of computation are shown.

Bibliographie

[1] P. Abdulla, M. B. Jonsson, M. Nilsson, “A survey of regular model checking ”, Proc. 15th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, 3170, 2004, 35–48 | Zbl

[2] K. Apt, D. Kozen, “Limits for automatic verification of finite-state concurrent systems”, Information Processing Letters, 15 (1986), 307–309 | DOI | MR

[3] M. Calder, A. Miller, “Five ways to use induction and symmetry in the verification of networks of processes by model-checking”, Automated Verification of Critical Systems (AvoCS 2002), 2002, 29–42

[4] E. Clarke, O. Grumberg, S. Jha, “Verifying parameterized networks using abstraction and regular languages”, 6-th International Conference on Concurrency Theory, 1995, 395–407

[5] E. Clarke, O. Grumberg, S. Jha, “Verifying parameterized networks”, ACM Transactions on Programming Languages and Systems, 19:5 (1997), 726–750 | DOI

[6] E. Emerson, K. Namjoshi, “Reasoning about rings”, Proceedings of 22th ACM Conf. on Principles of Programming Languages, 1995, 85–94

[7] E. Emerson, A. Sistla, “Symmetry and model checking”, Formal Methods in System Design, 9:1/2 (1996), 105–131 | DOI | MR

[8] G. Holzmann, A. Puri, “A minimized automaton representation of reachable states”, Software Tools for Technology Transfer, 3:1 (1998) | Zbl

[9] G. J. Holzmann, The SPIN Model Checker : Primer and Reference Manual, September, Addison-Wesley Professional, 2003

[10] C. N. Ip, D. L. Dill, “Verifying systems with replicated components in murphi”, Form. Methods Syst. Des., 14:3 (1999), 273–310 | DOI

[11] Y. Kesten, A. Pnueli, “Verification by finitary abstraction”, Information and Computation, 163 (2000), 203–243 | DOI | MR | Zbl

[12] R. P. Kurshan, K. McMillan, “A structural induction theorem for processes”, PODC '89: Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, ACM, New York, NY, USA, 1989, 239–247

[13] D. Lesens, “Invariants of parameterized binary tree networks as greatest fixpoints”, Algebraic Methodology and Software Technology, 1997, 337–350

[14] D. Lesens, N. Halbwachs, P. Raymond, “Automatic verification of parameterized linear networks of processes”, POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, New York, NY, USA, 1997, 346–357

[15] G. S. Manku, R. Hojati, R. K. Brayton, “Structural symmetry and model checking”, CAV'98: Proceedings of the 10th International Conference on Computer Aided Verification, Springer-Verlag, London, UK, 1998, 159–171 | MR

[16] R. Marelly, O. Grumberg, Gormel — grammar oriented model checker, Tech. Rep. 697, The Technion, Haifa, Israel, 1991

[17] M. Nilsson, Structural Symmetry and Model Checking, Ph.D. thesis, Uppsala University, Uppsala, Sweden, 2005, 157 pp. | Zbl

[18] R. Gerth, R. Kuiper, D. Peled, W. Penczek, “A partial order approach to branching time logic model checking”, Inf. Comput., 150:2 (1999), 132–152 | DOI | MR | Zbl

[19] W. Penczek, M. Szreter, R. Gerth, R. Kuiper, “Partial order reductions preserving simulations”, Proc. of Concurrency, Specification and Programming, 1999, 153–172

[20] R.Braden, Resource reservation protocol (RSVP), , 1997 http://tools.ietf.org/html/rfc2205

[21] E.Shahar, Tools and Techniques for Verifying Parameterized Systems, Ph.D. thesis, Weizmann Institute of Science, Israel, 2001, 120 pp.

[22] R. J. van Glabbeek, W. Peter Weijland, “Branching time and abstraction in bisimulation semantics”, J. ACM, 43:3 (1996), 555–600 | DOI | MR | Zbl

[23] E. Clarke, M. Talupur, T. Touili, H. Veith, “Verification by network decomposition”, LNCS, 3170, 2004, 276–291 | Zbl

[24] L. Wolper P., “Properties of large sets of processes with network invariants”, LNCS, 407, Springer-Verlag, Berlin, 1989, 68–80

[25] V. Zakharov, I. Konnov, “An invariant-based approach to the verification of asynchronous parameterized networks”, International Workshop on Invariant Generation (WING'07), RISC-Linz Report Series No. 07-07, RISC, July, Hagenberg, Austria, 2007, 41–55

[26] E. Klark, O. Gramberg, D. Peled, Verifikatsiya modelei programm: Model Checking, Izdatelstvo Moskovskogo tsentra nepreryvnogo matematicheskogo obrazovaniya, M., 2002

[27] I. Konnov, V. Zakharov, “Ob odnom podkhode k verifikatsii simmetrichnykh parametrizovannykh raspredelënnykh sistem”, Programmirovanie, 5 (2005), 3–17 | MR | Zbl