×

zbMATH — the first resource for mathematics

Generalized abstraction-refinement for game-based CTL lifted model checking. (English) Zbl 1460.68058
Summary: System families (Software Product Lines) are becoming omnipresent in application areas ranging from embedded system domains to system-level software and communication protocols. Software Product Line methods and architectures allow effective building many custom variants of a software system in these domains. In many of the applications, their rigorous verification and quality assurance are of paramount importance. Lifted model checking for system families is capable of verifying all their variants simultaneously in a single run by exploiting the similarities between the variants. The computational cost of lifted model checking still greatly depends on the number of variants (the size of configuration space), which is often huge. Variability abstractions have successfully addressed this configuration space explosion problem, giving rise to smaller abstract variability models with fewer abstract configurations. Abstract variability models are given as modal transition systems, which contain may (over-approximating) and must (under-approximating) transitions. Thus, they preserve both universal and existential CTL properties.
In this work, we bring two main contributions. First, we define a novel game-based approach for variability-specific abstraction and refinement for lifted model checking of the full CTL, interpreted over 3-valued semantics. We propose a direct algorithm for solving a 3-valued (abstract) lifted model checking game. In case the result of model checking an abstract variability model is indefinite, we suggest a new notion of refinement, which eliminates indefinite results. This provides an iterative incremental variability-specific abstraction and refinement framework, where refinement is applied only where indefinite results exist and definite results from previous iterations are reused. Second, we propose a new generalized definition of abstract variability models, given as so-called generalized modal transition systems, by introducing the notion of (must) hyper-transitions. This results in more precise abstract models in which more CTL formulae can be proved or disproved. We integrate the newly defined generalized abstract variability models in the existing abstraction-refinement framework for game-based lifted model checking of CTL. Finally, we evaluate the practicality of this approach on several system families.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
Software:
SPIN
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clements, P.; Northrop, L., Software Product Lines: Practices and Patterns (2001), Addison-Wesley
[2] Pohl, K.; Böckle, G.; van der Linden, F., Software Product Line Engineering: Foundations, Principles and Techniques (2005), Springer · Zbl 1075.68575
[3] Ebert, C.; Jones, C., Embedded software: facts, figures, and future, IEEE Comput., 42, 4, 42-52 (2009)
[4] Classen, A.; Cordy, M.; Schobbens, P.; Heymans, P.; Legay, A.; Raskin, J., Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking, IEEE Trans. Softw. Eng., 39, 8, 1069-1089 (2013)
[5] Classen, A.; Cordy, M.; Heymans, P.; Legay, A.; Schobbens, P., Model checking software product lines with SNIP, Int. J. Softw. Tools Technol. Transf., 14, 5, 589-612 (2012)
[6] Dimovski, A. S.; Al-Sibahi, A. S.; Brabrand, C.; Wasowski, A., Family-based model checking without a family-based model checker, (Model Checking Software - 22nd International Symposium, SPIN 2015, Proceedings. Model Checking Software - 22nd International Symposium, SPIN 2015, Proceedings, LNCS, vol. 9232 (2015), Springer), 282-299
[7] Dimovski, A. S.; Al-Sibahi, A. S.; Brabrand, C.; Wasowski, A., Efficient family-based model checking via variability abstractions, Int. J. Softw. Tools Technol. Transf., 19, 5, 585-603 (2017)
[8] Dimovski, A. S.; Wasowski, A., From transition systems to variability models and from lifted model checking back to UPPAAL, (Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, LNCS, vol. 10460 (2017), Springer), 249-268 · Zbl 1431.68074
[9] Dimovski, A. S., Abstract family-based model checking using modal featured transition systems: preservation of ctl^⋆, (Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Proceedings. Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Proceedings, LNCS, vol. 10802 (2018), Springer), 301-318 · Zbl 1423.68277
[10] Dimovski, A. S., {CTL*} family-based model checking using variability abstractions and modal transition systems, Int. J. Softw. Tools Technol. Transf., 22, 1, 35-55 (2020)
[11] Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronization skeletons using branching-time temporal logic, (Logics of Programs. Logics of Programs, Workshop, 1981. Logics of Programs. Logics of Programs, Workshop, 1981, LNCS, vol. 131 (1981), Springer), 52-71
[12] Stirling, C., Modal and Temporal Properties of Processes, Texts in Computer Science (2001), Springer · Zbl 0974.68056
[13] Shoham, S.; Grumberg, O., A game-based framework for CTL counterexamples and 3-valued abstraction-refinement, ACM Trans. Comput. Log., 9, 1, 1 (2007) · Zbl 1367.68203
[14] Shoham, S.; Grumberg, O., Compositional verification and 3-valued abstractions join forces, Inf. Comput., 208, 2, 178-202 (2010) · Zbl 1191.68416
[15] Dimovski, A. S.; Legay, A.; Wasowski, A., Variability abstraction and refinement for game-based lifted model checking of full CTL, (Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Proceedings. Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Proceedings, LNCS, vol. 11424 (2019), Springer), 192-209
[16] Shoham, S.; Grumberg, O., Monotonic abstraction-refinement for CTL, (Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Proceedings, LNCS, vol. 2988 (2004), Springer), 546-560 · Zbl 1126.68487
[17] Larsen, K. G.; Liu, X., Equation solving using modal transition systems, (Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS ’90) (1990), IEEE Computer Society), 108-117
[18] Classen, A.; Heymans, P.; Schobbens, P.-Y.; Legay, A., Symbolic model checking of software product lines, (Proceedings of the 33rd International Conference on Software Engineering. Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011 (2011), ACM), 321-330
[19] Baier, C.; Katoen, J., Principles of Model Checking (2008), MIT Press
[20] Larsen, K. G.; Thomsen, B., A modal process logic, (Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88) (1988), IEEE Computer Society), 203-210
[21] Godefroid, P.; Jagadeesan, R., On the expressiveness of 3-valued models, (Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, Proceedings. Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, Proceedings, LNCS, vol. 2575 (2003), Springer), 206-222 · Zbl 1022.68075
[22] Cousot, P., Partial completeness of abstract fixpoint checking, (Abstraction, Reformulation, and Approximation, 4th International Symposium, SARA 2000, Proceedings. Abstraction, Reformulation, and Approximation, 4th International Symposium, SARA 2000, Proceedings, LNCS, vol. 1864 (2000), Springer), 1-25 · Zbl 0989.68033
[23] Plath, M.; Ryan, M., Feature integration using a feature construct, Sci. Comput. Program., 41, 1, 53-84 (2001) · Zbl 0983.68236
[24] Ben-David, S.; Sterin, B.; Atlee, J. M.; Beidu, S., Symbolic model checking of product-line requirements using sat-based methods, (37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Volume 1 (2015), IEEE Computer Society), 189-199
[25] Dimovski, A. S.; Legay, A.; Wasowski, A., Variability abstraction and refinement for game-based lifted model checking of full ctl (extended version) (2019), CoRR
[26] Kozen, D., Results on the propositional mu-calculus, Theor. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007
[27] Grumberg, O.; Lange, M.; Leucker, M.; Shoham, S., Don’t know in the μ-calculus, (Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Proceedings. Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Proceedings, LNCS, vol. 3385 (2005), Springer), 233-249 · Zbl 1112.68090
[28] Larsen, K. G.; Nyman, U.; Wasowski, A., Modal I/O automata for interface and product line theories, (Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Proceedings. Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Proceedings, LNCS, vol. 4421 (2007), Springer), 64-79 · Zbl 1187.68296
[29] Cordy, M.; Classen, A.; Heymans, P.; Schobbens, P.; Legay, A., Provelines: a product line of verifiers for software product lines, (17th International SPLC 2013 Workshops (2013), ACM), 141-146
[30] Cordy, M.; Heymans, P.; Legay, A.; Schobbens, P.; Dawagne, B.; Leucker, M., Counterexample guided abstraction refinement of product-line behavioural models, (Cheung, S.; Orso, A.; Storey, M. D., Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE-22 (2014), ACM), 190-201
[31] Dimovski, A. S.; Wasowski, A., Variability-specific abstraction refinement for family-based model checking, (Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Proceedings. Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Proceedings, LNCS, vol. 10202 (2017)), 406-423 · Zbl 1430.68151
[32] Iosif-Lazar, A. F.; Melo, J.; Dimovski, A. S.; Brabrand, C.; Wasowski, A., Effective analysis of C programs by rewriting variability, Program. J., 1, 1, 1 (2017)
[33] Apel, S.; von Rhein, A.; Wendler, P.; Größlinger, A.; Beyer, D., Strategies for product-line verification: case studies and experiments, (35th International Conference on Software Engineering. 35th International Conference on Software Engineering, ICSE ’13 (2013), IEEE Computer Society), 482-491
[34] Dimovski, A. S.; Brabrand, C.; Wasowski, A., Variability abstractions: trading precision for speed in family-based analyses, (29th European Conference on Object-Oriented Programming. 29th European Conference on Object-Oriented Programming, ECOOP 2015. 29th European Conference on Object-Oriented Programming. 29th European Conference on Object-Oriented Programming, ECOOP 2015, LIPIcs, vol. 37 (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 247-270
[35] Midtgaard, J.; Dimovski, A. S.; Brabrand, C.; Wasowski, A., Systematic derivation of correct variability-aware program analyses, Sci. Comput. Program., 105, 145-170 (2015)
[36] Dimovski, A. S., Lifted static analysis using a binary decision diagram abstract domain, (Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences. Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2019 (2019), ACM), 102-114
[37] Dimovski, A. S.; Brabrand, C.; Wasowski, A., Finding suitable variability abstractions for lifted analysis, Formal Asp. Comput., 31, 2, 231-259 (2019) · Zbl 1425.68067
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.