×

zbMATH — the first resource for mathematics

Checking deadlock-freedom of parametric component-based systems. (English) Zbl 1455.68102
Summary: We propose an automated method for computing inductive invariants used to proving deadlock freedom of parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from interaction formulae defining the system architecture. The paper presents the theoretical foundations of the method and proves its soundness. It also reports on a preliminary experimental evaluation on several textbook examples.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Cubicle; CVC4; D-Finder
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] German, S. M.; Sistla, A. P., Reasoning about systems with many processes, J. ACM, 39, 3, 675-735 (1992) · Zbl 0799.68078
[2] Bloem, R.; Jacobs, S.; Khalimov, A.; Konnov, I.; Rubin, S.; Veith, H.; Widder, J., Decidability of Parameterized Verification, Synthesis Lectures on Distributed Computing Theory (2015), Morgan & Claypool Publishers
[3] Browne, M. C.; Clarke, E. M.; Grumberg, O., Reasoning about networks with many identical finite state processes, Inf. Comput., 81, 1, 13-31 (1989) · Zbl 0709.68610
[4] Emerson, E. A.; Namjoshi, K. S., Reasoning about rings, (Cytron, R. K.; Lee, P., Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1995), ACM Press), 85-94
[5] Aminof, B.; Kotek, T.; Rubin, S.; Spegni, F.; Veith, H., Parameterized model checking of rendezvous systems, Distrib. Comput., 31, 3, 187-222 (2018) · Zbl 1451.68165
[6] Emerson, E. A.; Kahlon, V., Reducing model checking of the many to the few, (McAllester, D. A., Automated Deduction - CADE-17, Proceedings of the 17th International Conference on Automated Deduction. Automated Deduction - CADE-17, Proceedings of the 17th International Conference on Automated Deduction, LNCS, vol. 1831 (2000), Springer), 236-254 · Zbl 0963.68109
[7] Außerlechner, S.; Jacobs, S.; Khalimov, A., Tight cutoffs for guarded protocols with fairness, (Jobstmann, B.; Leino, K. R.M., Verification, Model Checking, and Abstract Interpretation - Proceedings of the 17th International Conference. Verification, Model Checking, and Abstract Interpretation - Proceedings of the 17th International Conference, VMCAI 2016. Verification, Model Checking, and Abstract Interpretation - Proceedings of the 17th International Conference. Verification, Model Checking, and Abstract Interpretation - Proceedings of the 17th International Conference, VMCAI 2016, LNCS, vol. 9583 (2016), Springer), 476-494 · Zbl 06559872
[8] Jacobs, S.; Sakr, M., Analyzing guarded protocols: better cutoffs, more systems, more expressivity, (Dillig, I.; Palsberg, J., Verification, Model Checking, and Abstract Interpretation - Proceedings of the 19th International Conference. Verification, Model Checking, and Abstract Interpretation - Proceedings of the 19th International Conference, VMCAI 2018. Verification, Model Checking, and Abstract Interpretation - Proceedings of the 19th International Conference. Verification, Model Checking, and Abstract Interpretation - Proceedings of the 19th International Conference, VMCAI 2018, LNCS, vol. 10747 (2018), Springer), 247-268 · Zbl 1446.68105
[9] Abdulla, P. A.; Cerans, K.; Jonsson, B.; Tsay, Y., General decidability theorems for infinite-state systems, (Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS (1996), IEEE Computer Society), 313-321
[10] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theor. Comput. Sci., 256, 1-2, 63-92 (2001) · Zbl 0973.68170
[11] Kesten, Y.; Maler, O.; Marcus, M.; Pnueli, A.; Shahar, E., Symbolic model checking with rich assertional languages, Theor. Comput. Sci., 256, 1-2, 93-112 (2001) · Zbl 0973.68119
[12] Abdulla, P. A.; Delzanno, G.; Henda, N. B.; Rezine, A., Regular model checking without transducers (on efficient verification of parameterized systems), (Grumberg, O.; Huth, M., Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 13th International Conference. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 13th International Conference, TACAS 2007. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 13th International Conference. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 13th International Conference, TACAS 2007, LNCS, vol. 4424 (2007), Springer), 721-736 · Zbl 1186.68312
[13] Alberti, F.; Ghilardi, S.; Sharygina, N., A framework for the verification of parameterized infinite-state systems, (Giordano, L.; Gliozzi, V.; Pozzato, G. L., Proceedings of the 29th Italian Conference on Computational Logic. Proceedings of the 29th Italian Conference on Computational Logic, CEUR Workshop Proceedings, vol. 1195 (2014), CEUR-WS.org), 303-308
[14] Conchon, S.; Goel, A.; Krstic, S.; Mebsout, A.; Zaïdi, F., Cubicle: a parallel smt-based model checker for parameterized systems – tool paper, (Madhusudan, P.; Seshia, S. A., Computer Aided Verification, Proceedings of the 24th International Conference. Computer Aided Verification, Proceedings of the 24th International Conference, CAV 2012. Computer Aided Verification, Proceedings of the 24th International Conference. Computer Aided Verification, Proceedings of the 24th International Conference, CAV 2012, LNCS, vol. 7358 (2012), Springer), 718-724
[15] Baukus, K.; Bensalem, S.; Lakhnech, Y.; Stahl, K., Abstracting WS1S systems to verify parameterized networks, (Graf, S.; Schwartzbach, M. I., Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 6th International Conference. Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 6th International Conference, TACAS 2000. Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 6th International Conference. Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 6th International Conference, TACAS 2000, LNCS, vol. 1785 (2000), Springer), 188-203 · Zbl 0964.68096
[16] Bouajjani, A.; Habermehl, P.; Vojnar, T., Abstract regular model checking, (Alur, R.; Peled, D. A., Computer Aided Verification, Proceedings of the 16th International Conference. Computer Aided Verification, Proceedings of the 16th International Conference, CAV 2004. Computer Aided Verification, Proceedings of the 16th International Conference. Computer Aided Verification, Proceedings of the 16th International Conference, CAV 2004, LNCS, vol. 3114 (2004), Springer), 372-386 · Zbl 1103.68071
[17] Chen, Y.; Hong, C.; Lin, A. W.; Rümmer, P., Learning to prove safety over parameterised concurrent systems, (Stewart, D.; Weissenbacher, G., 2017 Formal Methods in Computer Aided Design. 2017 Formal Methods in Computer Aided Design, FMCAD 2017 (2017), IEEE), 76-83
[18] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (Aho, A. V.; Zilles, S. N.; Rosen, B. K., Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages (1979), ACM Press), 269-282
[19] Dams, D.; Lakhnech, Y.; Steffen, M., Iterating transducers, J. Log. Algebraic Methods Program., 52-53, 109-127 (2002) · Zbl 1008.68062
[20] Pnueli, A.; Ruah, S.; Zuck, L. D., Automatic deductive verification with invisible invariants, (Margaria, T.; Yi, W., Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 7th International Conference. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 7th International Conference, TACAS 2001. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 7th International Conference. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 7th International Conference, TACAS 2001, LNCS, vol. 2031 (2001), Springer), 82-97 · Zbl 0978.68539
[21] Clarke, E. M.; Talupur, M.; Veith, H., Environment abstraction for parameterized verification, (Emerson, E. A.; Namjoshi, K. S., Verification, Model Checking, and Abstract Interpretation, Proceedings of the 7th International Conference. Verification, Model Checking, and Abstract Interpretation, Proceedings of the 7th International Conference, VMCAI 2006. Verification, Model Checking, and Abstract Interpretation, Proceedings of the 7th International Conference. Verification, Model Checking, and Abstract Interpretation, Proceedings of the 7th International Conference, VMCAI 2006, LNCS, vol. 3855 (2006), Springer), 126-141 · Zbl 1176.68117
[22] Sifakis, J., Structural properties of Petri nets, (Winkowski, J., Mathematical Foundations of Computer Science 1978, Proceedings of the 7th Symposium. Mathematical Foundations of Computer Science 1978, Proceedings of the 7th Symposium, LNCS, vol. 64 (1978), Springer), 474-483
[23] Bensalem, S.; Bozga, M.; Nguyen, T.; Sifakis, J., D-finder: a tool for compositional deadlock detection and verification, (Bouajjani, A.; Maler, O., Computer Aided Verification, Proceedings of the 21st International Conference. Computer Aided Verification, Proceedings of the 21st International Conference, CAV 2009. Computer Aided Verification, Proceedings of the 21st International Conference. Computer Aided Verification, Proceedings of the 21st International Conference, CAV 2009, LNCS, vol. 5643 (2009), Springer), 614-619
[24] Kuncak, V.; Nguyen, H. H.; Rinard, M. C., Deciding Boolean algebra with Presburger arithmetic, J. Autom. Reason., 36, 3, 213-239 (2006) · Zbl 1112.03011
[25] Barrett, C. W.; Conway, C. L.; Deters, M.; Hadarean, L.; Jovanovic, D.; King, T.; Reynolds, A.; Tinelli, C., CVC4, (Gopalakrishnan, G.; Qadeer, S., Computer Aided Verification, Proceedings of the 23rd International Conference. Computer Aided Verification, Proceedings of the 23rd International Conference, CAV 2011. Computer Aided Verification, Proceedings of the 23rd International Conference. Computer Aided Verification, Proceedings of the 23rd International Conference, CAV 2011, LNCS, vol. 6806 (2011), Springer), 171-177
[26] Basu, A.; Bensalem, S.; Bozga, M.; Combaz, J.; Jaber, M.; Nguyen, T.; Sifakis, J., Rigorous component-based system design using the BIP framework, IEEE Softw., 28, 3, 41-48 (2011)
[27] Lowenheim, L., Über Möglichkeiten im Relativkalkül, Math. Ann., 470, 76-447 (1915) · JFM 45.0108.01
[28] Bansal, K.; Reynolds, A.; Barrett, C. W.; Tinelli, C., A new decision procedure for finite sets and cardinality constraints in SMT, (Olivetti, N.; Tiwari, A., Automated Reasoning - Proceedings of the 8th International Joint Conference. Automated Reasoning - Proceedings of the 8th International Joint Conference, IJCAR 2016. Automated Reasoning - Proceedings of the 8th International Joint Conference. Automated Reasoning - Proceedings of the 8th International Joint Conference, IJCAR 2016, LNCS, vol. 9706 (2016), Springer), 82-98 · Zbl 06623255
[29] Bozga, M.; Iosif, R.; Sifakis, J., Checking deadlock-freedom of parametric component-based systems, (Vojnar, T.; Zhang, L., Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 25th International Conference. Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 25th International Conference, TACAS 2019. Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 25th International Conference. Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 25th International Conference, TACAS 2019, LNCS, vol. 11428 (2019), Springer), 3-20
[30] Skolem, T., Untersuchungen über die Axiome des Klassenkalküls and über “Produktations- und Summationsprobleme”, welche gewisse Klassen von Aussagen betreffen (1919), Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, no. 3, Oslo
[31] Schrijver, A., Combinatorial Optimization - Polyhedra and Efficiency, vol. A (2003), Springer
[32] Delzanno, G., Automatic verification of parameterized cache coherence protocols, (Emerson, E. A.; Sistla, A. P., Computer Aided Verification, Proceedings of the 12th International Conference. Computer Aided Verification, Proceedings of the 12th International Conference, CAV 2000. Computer Aided Verification, Proceedings of the 12th International Conference. Computer Aided Verification, Proceedings of the 12th International Conference, CAV 2000, LNCS, vol. 1855 (2000), Springer), 53-68 · Zbl 0974.68500
[33] Bozga, M.; Esparza, J.; Iosif, R.; Sifakis, J.; Welzel, C., Structural invariants for the verification of systems with parameterized architectures, (Biere, A.; Parker, D., Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 26th International Conference. Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 26th International Conference, TACAS 2020. Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 26th International Conference. Tools and Algorithms for the Construction and Analysis of Systems - Proceedings of the 26th International Conference, TACAS 2020, LNCS, vol. 12078 (2020), Springer), 228-246
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.