×

Model checking parameterized systems. (English) Zbl 1392.68223

Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 685-725 (2018).
Summary: We consider the model-checking problem for a particular class of parameterized systems: systems that consist of arbitrary numbers of components. The task is to show correctness regardless of the number of components. The term parameterized refers to the fact that the size of the system is a parameter of the verification problem. Examples of parameterized systems include mutual exclusion algorithms, bus protocols, networking protocols, cache coherence protocols, web services, and sensor networks. In this chapter, we will give four examples of techniques that have been used (among many others) for the verification of parameterized systems.
For the entire collection see [Zbl 1390.68001].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

MONA; Mosel
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] 1. Abadi, M., Lamport, L.: Composing specifications. In: ACM Transactions on Programming Languages and Systems. ACM, New York (1993)
[2] 2. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Symp. on Logic in Computer Science (LICS), pp. 313-321. IEEE, Piscataway (1996)
[3] 3. Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 721-736. Springer, Heidelberg (2007) · Zbl 1186.68312
[4] 4. Abdulla, P.A., Haziza, F., Hol’ik, L.: All for the price of few (parameterized verification through view abstraction). In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 7737, pp. 476-495. Springer, Heidelberg (2013) · Zbl 1426.68160
[5] 5. Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J.: Regular model checking made simple and efficient. In: Brim, L., Jancar, P., Kretínský, M., Kucera, A. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 2421, pp. 116-130. Springer, Heidelberg (2002) · Zbl 1012.68134
[6] 6. Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J., Saksena, M.: Regular model checking for LTL(MSO). In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 348-360. Springer, Heidelberg (2004) · Zbl 1103.68070
[7] 7. Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 3170, pp. 35-48. Springer, Heidelberg (2004) · Zbl 1099.68055
[8] 8. Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307-309 (1986)
[9] 9. Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 221-234. Springer, Heidelberg (2001) · Zbl 0991.68541
[10] 10. Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized verification of a cache coherence protocol: safety and liveness. In: Cortesi, A. (ed.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 2294, pp. 317-330. Springer, Heidelberg (2002) · Zbl 1057.68620
[11] 11. Bhattacharya, R., German, S.M., Gopalakrishnan, G.: Exploiting symmetry and transactions for partial order reduction of rule based specifications. In: Valmari, A. (ed.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol. 3925. Springer, Heidelberg (2006) · Zbl 1178.68335
[12] 12. Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool, San Rafael (2015) · Zbl 1400.68006
[13] 13. Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large (extended abstract). In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 223-235. Springer, Heidelberg (2003) · Zbl 1278.68157
[14] 14. Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 561-575. Springer, Heidelberg (2004) · Zbl 1126.68469
[15] 15. Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf. 14(2), 167-191 (2012) · Zbl 1273.68221
[16] 16. Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 372-386. Springer, Heidelberg (2004) · Zbl 1103.68071
[17] 17. Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 539-554. Springer, Heidelberg (2002) · Zbl 1010.68085
[18] 18. Browne, M., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13-31 (1989) · Zbl 0709.68610
[19] 19. Chen, X., Yang, Y., DeLisi, M., Gopalakrishnan, G., Chou, C.T.: Hierarchical cache coherence protocol verification one level at a time through assume guarantee. In: High Level Design Validation and Test Workshop (HLDVT). IEEE, Piscataway (2007)
[20] 20. Chou, C.T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 3312. Springer, Heidelberg (2004) · Zbl 1117.68423
[21] 21. Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks using abstraction and regular languages. ACM Trans. Program. Lang. Syst. 19(5), 726-750 (1997)
[22] 22. Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1/2), 77-104 (1996)
[23] 23. Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 3855, pp. 126-141. Springer, Heidelberg (2006) · Zbl 1176.68117
[24] 24. Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1633. Springer, Heidelberg (1999) · Zbl 1046.68589
[25] 25. Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 53-68. Springer, Heidelberg (2000) · Zbl 0974.68500
[26] 26. Delzanno, G.: Verification of consistency protocols via infinite-state symbolic model checking. In: Bolognesi, T., Latella, D. (eds.) Formal Methods for Distributed System Development (FORTE), pp. 171-186. Springer, Heidelberg (2000)
[27] 27. Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 6269, pp. 313-327. Springer, Heidelberg (2010) · Zbl 1287.68106
[28] 28. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with · JFM 44.0220.02
[29] 29. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 1831, pp. 236-254. Springer, Heidelberg (2000) · Zbl 0963.68109
[30] 30. Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) Correct Hardware Design and Verification Methods (CHARME). LNCS, vol. 2860, pp. 247-262. Springer, Heidelberg (2003) · Zbl 1179.68013
[31] 31. Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: Symp. on Logic in Computer Science (LICS), pp. 361-370. IEEE, Piscataway (2003) · Zbl 1031.68548
[32] 32. Emerson, E.A., Kahlon, V.: Rapid parameterized model checking of snoopy cache coherence protocols. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2619, pp. 144-159. Springer, Heidelberg (2003) · Zbl 1031.68548
[33] 33. Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Cytron, R.K., Lee, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 85-94. ACM, New York (1995)
[34] 34. Emerson, E.A., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1102, pp. 87-98. Springer, Heidelberg (1996)
[35] 35. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des. 9(1/2), 105-131 (1996)
[36] 36. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Symp. on Logic in Computer Science (LICS), pp. 352-359. IEEE, Piscataway (1999)
[37] 37. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Syst. 256(1-2), 63-92 (2001) · Zbl 0973.68170
[38] 38. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675-735 (1992) · Zbl 0799.68078
[39] 39. Henriksen, J.G., Jensen, J.L., Jørgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1019, pp. 89-110. Springer, Heidelberg (1995)
[40] 40. Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3) 2(7) (1952) · Zbl 0047.03402
[41] 41. Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Proc. Conf. on Computer Hardware Description Languages and Their Applications, pp. 97-111 (1993)
[42] 42. Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1/2), 41-75 (1996)
[43] 43. Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147-195 (1969) · Zbl 0198.32603
[44] 44. Kelb, P., Margaria, T., Mendler, M., Gsottberger, C.: Mosel: a flexible toolset for monadic second-order logic. In: Brinksma, E. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1217, pp. 183-202. Springer, Heidelberg (1997)
[45] 45. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 424-435. Springer, Heidelberg (1997) · Zbl 0973.68119
[46] 46. Krstic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: Automated Verification of Infinite State Systems (2005)
[47] 47. Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Rudnicki, P. (ed.) ACM Symp. on Principles of Distributed Computing (PODC), pp. 239-247. ACM, New York (1989)
[48] 48. Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 135-147. Springer, Heidelberg (2004) · Zbl 1103.68627
[49] 49. Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453-455 (1974) · Zbl 0281.68004
[50] 50. Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parametrized linear networks of processes. In: Boehm, H.-J., Steele, G.L. Jr. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 101-105. ACM, New York (1996) · Zbl 0973.68145
[51] 51. Maidl, M.: A unifying model checking approach for safety properties of parameterized systems. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 311-323. Springer, Heidelberg (2001) · Zbl 0991.68047
[52] 52. McMillan, K.L.: Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1427. Springer, Heidelberg (1998)
[53] 53. McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods (CHARME). LNCS, vol. 1703. Springer, Heidelberg (1999) · Zbl 0957.68068
[54] 54. McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol. 2144, pp. 179-195. Springer, Heidelberg (2001) · Zbl 1002.68674
[55] 55. Misra, J., Chandy, K.M.: Proofs of networks of processes. In: IEEE Transactions on Software Engineering, vol. SE-7. IEEE, Piscataway (1981) · Zbl 0468.68030
[56] 56. O’Leary, J., Talupur, M., Tuttle, M.R.: Protocol Verification using Flows: Parameterized Verification using Message Flows. Formal Methods in Computer Aided Design (FMCAD). IEEE, Piscataway (2009)
[57] 57. Park, S., Dill, D.L.: Verification of flash cache coherence protocol by aggregation of distributed transactions. In: SPAA ’96: Proceedings of the Eighth Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 288-296. ACM, New York (1996)
[58] 58. Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 82-97. Springer, Heidelberg (2001) · Zbl 0978.68539
[59] 59. Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (
[60] 60. Roychoudhury, A., Ramakrishnan, I.V.: Automated inductive verification of parameterized protocols. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 25-37. Springer, Heidelberg (2001) · Zbl 0991.68555
[61] 61. Sethi, D., Talupur, M., Schwartz-Narbonne, D., Malik, S.: Parameterized model checking of fine grained concurrency. In: Donaldson, A.F., Parker, D. (eds.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol. 7385. Springer, Heidelberg (2012)
[62] 62. Shtadler, Z., Grumberg, O.: Network grammars, communication behaviors and automatic verification. In: Sifakis, J. (ed.) Workshop on Automatic Verification Methods for Finite State Systems. LNCS, pp. 151-166. Springer, Heidelberg (1989)
[63] 63. Sistla, A.P., Gyuris, V.: Parameterized verification of linear networks using automata as invariants. Form. Asp. Comput. 11, 402-425 (1999) · Zbl 0955.68069
[64] 64. Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213-214 (1988) · Zbl 0664.68048
[65] 65. Szymanski, B.K.: A simple solution to Lamport’s concurrent programming problem with linear wait. In: Lenfant, J. (ed.) International Conference on Supercomputing (ICS), pp. 621-626. ACM, New York (1988)
[66] 66. Talupur, M., Krstic, S., O’Leary, J., Tuttle, M.R.: Parametric verification of industrial strength cache coherence protocols. In: Proc. Workshop on Design of Correct Circuits (DCC) (2008)
[67] 67. Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: Cimatti, A., Jones, R.B. (eds.) Formal Methods in Computer Aided Design (FMCAD). IEEE, Piscataway (2008)
[68] 68. Topnik, C., Wilhelm, E., Margaria, T., Steffen, B.: jMosel: a stand-alone tool and jABC plugin for M2L(Str). In: Valmari, A. (ed.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol. 3925, pp. 293-298. Springer, Heidelberg (2006)
[69] 69. Touili, T.: Regular model checking using widening techniques. Electron. Notes Theor. Comput. Sci. 50(4), 342-356 (2001) · Zbl 1262.68130
[70] 70. Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Workshop on Automatic Verification Methods for Finite State Systems, pp. 68-81. Springer, Heidelberg (1989)
[71] 71. Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30(3-4), 139-169 (2004) · Zbl 1022.68580
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.