{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:04:20Z","timestamp":1779087860516,"version":"3.51.4"},"reference-count":91,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,10,23]],"date-time":"2021-10-23T00:00:00Z","timestamp":1634947200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,10,23]],"date-time":"2021-10-23T00:00:00Z","timestamp":1634947200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100006692","name":"Universit\u00e0 degli Studi di Torino","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100006692","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2022,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called <jats:italic>dead transitions<\/jats:italic>) or, on the contrary, can be executed in all products (so called <jats:italic>false optional transitions<\/jats:italic>). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called <jats:italic>hidden deadlock states<\/jats:italic>). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification\u2014if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.<\/jats:p>","DOI":"10.1007\/s10664-020-09930-8","type":"journal-article","created":{"date-parts":[[2021,10,23]],"date-time":"2021-10-23T06:02:43Z","timestamp":1634968963000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Efficient static analysis and verification of featured transition systems"],"prefix":"10.1007","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8109-1706","authenticated-orcid":false,"given":"Ferruccio","family":"Damiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Lienhardt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4562-8777","authenticated-orcid":false,"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4126-0170","authenticated-orcid":false,"given":"Luca","family":"Paolini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,23]]},"reference":[{"issue":"21","key":"9930_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"4","author":"B Alpern","year":"1985","unstructured":"Alpern B, Schneider FB (1985) Defining liveness. Inf Process Lett 4(21):181\u2013185. https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","journal-title":"Inf Process Lett"},{"key":"9930_CR2","doi-asserted-by":"publisher","unstructured":"Apel S, Batory D, K\u00e4stner C., Saake G (2013) Feature-oriented software product lines: concepts and implementation, Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-642-37521-7","DOI":"10.1007\/978-3-642-37521-7"},{"key":"9930_CR3","unstructured":"Asirelli P, ter Beek MH, Fantechi A, Gnesi S (2009) Deontic logics for modeling behavioural variability. In: Benavides D, Metzger A, Eisenecker U (eds) Proceedings of the 3rd international workshop on variability modelling of software-intensive systems (VaMoS\u201909), ICB Research Report, vol 29, pp 71\u201376. Universit\u00e4t Duisburg-Essen"},{"key":"9930_CR4","doi-asserted-by":"publisher","unstructured":"Asirelli P, ter Beek MH, Fantechi A, Gnesi S (2010) A logical framework to deal with variability. In: M\u00e9ry D, Merz S (eds) Proceedings of the 8th international conference on integrated formal methods (IFM\u201910), LNCS, vol 6396, Springer, pp 43\u201358. https:\/\/doi.org\/10.1007\/978-3-642-16265-7_5","DOI":"10.1007\/978-3-642-16265-7_5"},{"key":"9930_CR5","doi-asserted-by":"publisher","unstructured":"Asirelli P, ter Beek MH, Fantechi A, Gnesi S (2011) Formal description of variability in product families. In: Proceedings of the 15th international software product lines conference (SPLC\u201911), IEEE, pp 130\u2013139. https:\/\/doi.org\/10.1109\/SPLC.2011.34","DOI":"10.1109\/SPLC.2011.34"},{"key":"9930_CR6","doi-asserted-by":"publisher","unstructured":"Audemard G, Lagniez JM, Szczepanski N, Tabary S (2016) An adaptive parallel SAT solver. In: Rueher M (ed) Proceedings of the 22nd international conference on principles and practice of constraint programming (CP\u201916), LNCS, vol 9892, Springer, pp 30\u201348. https:\/\/doi.org\/10.1007\/978-3-319-44953-1_3","DOI":"10.1007\/978-3-319-44953-1_3"},{"issue":"3","key":"9930_CR7","doi-asserted-by":"publisher","first-page":"14","DOI":"10.4204\/EPTCS.182.2","volume":"220","author":"T Belder","year":"2015","unstructured":"Belder T, ter Beek MH, de Vink EP (2015) Coherent branching feature bisimulation. Electron Proc Theor Comput Sci 220(3):14\u201330. https:\/\/doi.org\/10.4204\/EPTCS.182.2","journal-title":"Electron Proc Theor Comput Sci"},{"issue":"6","key":"9930_CR8","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1016\/j.is.2010.01.001","volume":"35","author":"D Benavides","year":"2010","unstructured":"Benavides D, Segura S, Ruiz-Cort\u00e9s A (2010) Automated analysis of feature models 20 years later: a literature review. Inf Syst 35(6):615\u2013636. https:\/\/doi.org\/10.1016\/j.is.2010.01.001","journal-title":"Inf Syst"},{"key":"9930_CR9","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.scico.2015.06.005","volume":"123","author":"H Beohar","year":"2016","unstructured":"Beohar H, Varshosaz M, Mousavi MR (2016) Basic behavioral models for software product lines: Expressiveness and testing pre-orders. Sci Comput Program 123:42\u201360. https:\/\/doi.org\/10.1016\/j.scico.2015.06.005","journal-title":"Sci Comput Program"},{"key":"9930_CR10","doi-asserted-by":"publisher","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive theorem proving and program development \u2014 Coq\u2019Art: the calculus of inductive constructions. Texts in theoretical computer science. An EATCS series, Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9930_CR11","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner N, Phan AD, Fleckenstein L (2015) \u03bd Z \u2013 An optimizing SMT solver. In: Baier C, Tinelli C (eds) Proceedings of the 21st international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201915), LNCS, vol 9035, Springer, pp 194\u2013199. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"9930_CR12","doi-asserted-by":"publisher","unstructured":"Bodden E, Tol\u00eado T, Ribeiro M, Brabrand C, Borba P, Mezini M (2013) SPLLIFT \u2014 Statically analyzing software product lines in minutes instead of years. In: Proceedings of the 34th conference on programming language design and implementation (PLDI\u201913), ACM, pp 355\u2013364. https:\/\/doi.org\/10.1145\/2491956.2491976","DOI":"10.1145\/2491956.2491976"},{"key":"9930_CR13","doi-asserted-by":"publisher","unstructured":"Bunte O, Groote JF, Keiren JJA, Laveaux M, Neele T, de Vink EP, Wesselink W, Wijs A, Willemse TAC (2019) The mCRL2 toolset for analysing concurrent systems: improvements in expressivity and usability. In: Vojnar T., Zhang L. (eds) Proceedings of the 25th international conference on tools and algorithms for the construction and analysis of systems (TACAS19), LNCS, vol 11428, Springer, pp 21\u201339. https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"9930_CR14","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.scico.2017.10.013","volume":"152","author":"TM Castro","year":"2018","unstructured":"Castro TM, Lanna A, Alves V, Teixeira L, Apel S, Schobbens PY (2018) All roads lead to Rome: Commuting strategies for product-line reliability analysis. Sci Comput Program 152:116\u2013160. https:\/\/doi.org\/10.1016\/j.scico.2017.10.013","journal-title":"Sci Comput Program"},{"key":"9930_CR15","volume-title":"Secure programming with static analysis","author":"B Chess","year":"2007","unstructured":"Chess B, West J (2007) Secure programming with static analysis. Addison-Wesley, Boston"},{"issue":"1","key":"9930_CR16","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-017-0432-4","volume":"30","author":"P Chrszon","year":"2018","unstructured":"Chrszon P, Dubslaff C, Kl\u00fcppelholz S, Baier C (2018) ProFeat: feature-oriented engineering for family-based probabilistic model checking. Form Asp Comp 30(1):45\u201375. https:\/\/doi.org\/10.1007\/s00165-017-0432-4","journal-title":"Form Asp Comp"},{"key":"9930_CR17","unstructured":"Classen A (2010) Modelling with FTS: a collection of illustrative examples. Tech. Rep. P-CS-TR SPLMC-00000001. University of Namur"},{"key":"9930_CR18","unstructured":"Classen A (2011) Modelling and model checking variability-intensive systems. Ph.D. thesis, University of Namur"},{"issue":"5","key":"9930_CR19","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-012-0234-1","volume":"14","author":"A Classen","year":"2012","unstructured":"Classen A, Cordy M, Heymans P, Legay A, Schobbens PY (2012) Model checking software product lines with SNIP. Int J Softw Tools Technol Transf 14(5):589\u2013612. https:\/\/doi.org\/10.1007\/s10009-012-0234-1","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"B","key":"9930_CR20","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1016\/j.scico.2013.09.019","volume":"80","author":"A Classen","year":"2014","unstructured":"Classen A, Cordy M, Heymans P, Legay A, Schobbens PY (2014) Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci Comput Program 80(B):416\u2013439. https:\/\/doi.org\/10.1016\/j.scico.2013.09.019","journal-title":"Sci Comput Program"},{"issue":"8","key":"9930_CR21","doi-asserted-by":"publisher","first-page":"1069","DOI":"10.1109\/TSE.2012.86","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen A, Cordy M, Schobbens PY, Heymans P, Legay A, Raskin JF (2013) Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans Softw Eng 39 (8):1069\u20131089. https:\/\/doi.org\/10.1109\/TSE.2012.86","journal-title":"IEEE Trans Softw Eng"},{"key":"9930_CR22","doi-asserted-by":"publisher","unstructured":"Classen A, Heymans P, Schobbens PY, Legay A, Raskin JF (2010) Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd international conference on software engineering (ICSE\u201910), ACM, pp 335\u2013344. https:\/\/doi.org\/10.1145\/1806799.1806850","DOI":"10.1145\/1806799.1806850"},{"key":"9930_CR23","doi-asserted-by":"publisher","unstructured":"Cook SA (1971) The complexity of theorem-proving procedures. In: Proceedings of the 3rd annual symposium on theory of computing (STOC\u201971), ACM, pp 151\u2013158. https:\/\/doi.org\/10.1145\/800157.805047","DOI":"10.1145\/800157.805047"},{"key":"9930_CR24","doi-asserted-by":"publisher","unstructured":"Cordy M, Classen A, Heymans P, Schobbens PY, Legay A (2013a) ProVeLines: a product line of verifiers for software product lines. In: Proceedings of the 17th international software product line conference (SPLC\u201913), vol 2, ACM, pp 141\u2013146. https:\/\/doi.org\/10.1145\/2499777.2499781","DOI":"10.1145\/2499777.2499781"},{"key":"9930_CR25","doi-asserted-by":"publisher","unstructured":"Cordy M, Schobbens PY, Heymans P, Legay A (2013b) Beyond Boolean product-line model checking: dealing with feature attributes and multi-features. In: Proceedings of the 35th international conference on software engineering (ICSE\u201913), IEEE, pp 472\u2013481. https:\/\/doi.org\/10.1109\/ICSE.2013.6606593","DOI":"10.1109\/ICSE.2013.6606593"},{"key":"9930_CR26","doi-asserted-by":"publisher","unstructured":"Cordy M, Classen A, Perrouin G, Schobbens PY, Heymans P, Legay A (2012) Simulation-based abstractions for software product-line model checking. In: Proceedings of the 34th international conference on software engineering (ICSE\u201912), IEEE, pp 672\u2013682. https:\/\/doi.org\/10.1109\/ICSE.2012.6227150","DOI":"10.1109\/ICSE.2012.6227150"},{"key":"9930_CR27","doi-asserted-by":"publisher","unstructured":"Cordy M, Devroey X, Legay A, Perrouin G, Classen A, Heymans P, Schobbens PY, Raskin JF (2019) A decade of featured transition systems. In: ter Beek MH, Fantechi A, Semini L (eds) From software engineering to formal methods and tools, and back, LNCS, vol 11865, Springer, pp 285\u2013312. https:\/\/doi.org\/10.1007\/978-3-030-30985-5_18","DOI":"10.1007\/978-3-030-30985-5_18"},{"key":"9930_CR28","doi-asserted-by":"publisher","unstructured":"Cranen S, Groote JF, Keiren JJA, Stappers FPM, de Vink EP, Wesselink W, Willemse TAC (2013) An overview of the mCRL2 toolset and its recent advances. In: Piterman N, Smolka SA (eds) Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201913), LNCS, vol 7795, Springer, pp 199\u2013213, DOI https:\/\/doi.org\/10.1007\/978-3-642-36742-7_15, (to appear in print)","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"9930_CR29","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.scico.2018.11.005","volume":"172","author":"F Damiani","year":"2019","unstructured":"Damiani F, Lienhardt M, Paolini L (2019) A formal model for multi software product lines. Sci Comput Program 172:203\u2013231. https:\/\/doi.org\/10.1016\/j.scico.2018.11.005","journal-title":"Sci Comput Program"},{"key":"9930_CR30","doi-asserted-by":"publisher","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201908), LNCS. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24, vol 4963. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9930_CR31","doi-asserted-by":"publisher","unstructured":"Delaware B, Cook WR, Batory D (2009) Fitting the pieces together: a machine-checked model of safe composition. In: Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering (ESEC\/FSE\u201909), ACM, pp 243\u2013252. https:\/\/doi.org\/10.1145\/1595696.1595733","DOI":"10.1145\/1595696.1595733"},{"issue":"1","key":"9930_CR32","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s10270-015-0479-8","volume":"16","author":"X Devroey","year":"2017","unstructured":"Devroey X, Perrouin G, Cordy M, Samih H, Legay A, Schobbens PY, Heymans P (2017) Statistical prioritization for software product line testing: an experience report. Softw Syst Model 16(1):153\u2013171. https:\/\/doi.org\/10.1007\/s10270-015-0479-8","journal-title":"Softw Syst Model"},{"key":"9930_CR33","doi-asserted-by":"publisher","unstructured":"Devroey X, Perrouin G, Cordy M, Schobbens PY, Legay A, Heymans P (2014a) Towards statistical prioritization for software product lines testing. In: Proceedings of the 8th international workshop on variability modelling of software-intensive systems (VaMoS\u201914), ACM, pp 10:1\u201310:7. https:\/\/doi.org\/10.1145\/2556624.2556635","DOI":"10.1145\/2556624.2556635"},{"key":"9930_CR34","doi-asserted-by":"publisher","unstructured":"Devroey X, Perrouin G, Legay A, Cordy M, Schobbens PY, Heymans P (2014b) Coverage criteria for behavioural testing of software product lines. In: Margaria T, Steffen B (eds) Proceedings of the 6th international symposium on leveraging applications of formal methods, verification and validation (ISoLA\u201914), LNCS, vol 8802, Springer, pp 336\u2013350. https:\/\/doi.org\/10.1007\/978-3-662-45234-9_24","DOI":"10.1007\/978-3-662-45234-9_24"},{"key":"9930_CR35","doi-asserted-by":"publisher","unstructured":"Devroey X, Perrouin G, Schobbens PY (2014c) Abstract test case generation for behavioural testing of software product lines. In: Proceedings of the 18th international software product line conference (SPLC\u201914), vol 2, ACM, pp 86\u201393. https:\/\/doi.org\/10.1145\/2647908.2655971","DOI":"10.1145\/2647908.2655971"},{"key":"9930_CR36","doi-asserted-by":"publisher","unstructured":"Devroey X, Perrouin G, Legay A, Schobbens PY, Heymans P (2015) Covering SPL behaviour with sampled configurations: an initial assessment. In: Proceedings of the 9th international workshop on variability modelling of software-intensive systems (VaMoS\u201915), ACM, pp 59:59\u201359:66. https:\/\/doi.org\/10.1145\/2701319.2701325","DOI":"10.1145\/2701319.2701325"},{"key":"9930_CR37","doi-asserted-by":"publisher","unstructured":"Devroey X, Perrouin G, Legay A, Schobbens PY, Heymans P (2016a) Search-based similarity-driven behavioural SPL testing. In: Proceedings of the 10th international workshop on variability modelling of software-intensive systems (VaMoS\u201916), ACM, pp 89\u201396. https:\/\/doi.org\/10.1145\/2866614.2866627","DOI":"10.1145\/2866614.2866627"},{"key":"9930_CR38","doi-asserted-by":"publisher","unstructured":"Devroey X, Perrouin G, Papadakis M, Legay A, Schobbens PY, Heymans P (2016b) Featured model-based mutation analysis. In: Proceedings of the 38th international conference on software engineering (ICSE\u201916), ACM, pp 655\u2013666. https:\/\/doi.org\/10.1145\/2884781.2884821","DOI":"10.1145\/2884781.2884821"},{"key":"9930_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2018.03.010","volume":"141","author":"X Devroey","year":"2018","unstructured":"Devroey X, Perrouin G, Papadakis M, Legay A, Schobbens PY, Heymans P (2018) Model-based mutant equivalence detection using automata language equivalence and simulations. J Syst Softw 141:1\u201315. https:\/\/doi.org\/10.1016\/j.jss.2018.03.010","journal-title":"J Syst Softw"},{"issue":"1","key":"9930_CR40","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10009-019-00528-0","volume":"22","author":"AS Dimovski","year":"2020","unstructured":"Dimovski AS (2020) CTL\u2217 family-based model checking using variability abstractions and modal transition systems. Int J Softw Tools Technol Transf 22(1):35\u201355. https:\/\/doi.org\/10.1007\/s10009-019-00528-0","journal-title":"Int J Softw Tools Technol Transf"},{"key":"9930_CR41","doi-asserted-by":"publisher","unstructured":"Dimovski AS, Legay A, W\u0119sowski A (2019) Variability abstraction and refinement for game-based lifted model checking of full CTL. In: H\u00e4hnle R, van der Aalst W (eds) Proceedings of the 22nd international conference on fundamental approaches to software engineering (FASE\u201919), LNCS, vol 11424, Springer, pp 192\u2013209. https:\/\/doi.org\/10.1007\/978-3-030-16722-6_11","DOI":"10.1007\/978-3-030-16722-6_11"},{"key":"9930_CR42","doi-asserted-by":"publisher","unstructured":"Dimovski AS (2018) Abstract family-based model checking using modal featured transition s ystems: preservation of CTL\u2217. In: Russo A, Sch\u00fcrr A (eds) Proceedings of the 21st international conference on fundamental approaches to software Engineering (FASE\u201918), LNCS, vol 10802, Springer, pp 301\u2013318. https:\/\/doi.org\/10.1007\/978-3-319-89363-1_17","DOI":"10.1007\/978-3-319-89363-1_17"},{"issue":"19","key":"9930_CR43","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10009-016-0425-2","volume":"5","author":"AS Dimovski","year":"2017","unstructured":"Dimovski AS, Al-Sibahi AS, Brabrand C, W\u0119sowski A (2017) Efficient family-based model checking via variability abstractions. Int J Softw Tools Technol Transf 5(19):585\u2013603. https:\/\/doi.org\/10.1007\/s10009-016-0425-2","journal-title":"Int J Softw Tools Technol Transf"},{"key":"9930_CR44","doi-asserted-by":"publisher","unstructured":"Dimovski AS, Al-Sibahi AS, Brabrand C, W\u0119sowski A (2015) Proceedings of the 22nd international SPIN symposium on model checking of software (SPIN\u201915), LNCS, vol 9232, Springer, pp 282\u2013299. In: Fischer B, Geldenhuys J (eds), DOI https:\/\/doi.org\/10.1007\/978-3-319-23404-5_18, (to appear in print)","DOI":"10.1007\/978-3-319-23404-5_18"},{"key":"9930_CR45","doi-asserted-by":"publisher","unstructured":"Dimovski AS, W\u0119sowski A (2017) Variability-specific abstraction refinement for family-based model checking. In: Huisman M, Rubin J (eds) Proceedings of the 20th international conference on fundamental approaches to software engineering (FASE\u201917), LNCS, vol 10202, Springer, pp 406\u2013423. https:\/\/doi.org\/10.1007\/978-3-662-54494-5_24","DOI":"10.1007\/978-3-662-54494-5_24"},{"key":"9930_CR46","doi-asserted-by":"publisher","unstructured":"Dubslaff C (2019) Compositional feature-oriented systems. In: \u00d6lveczky PC, Sala\u00fcn G (eds) Proceedings of the 17th international conference on software engineering and formal methods (SEFM\u201919), LNCS, vol 11724, Springer, pp 162\u2013180. https:\/\/doi.org\/10.1007\/978-3-030-30446-1_9","DOI":"10.1007\/978-3-030-30446-1_9"},{"key":"9930_CR47","doi-asserted-by":"publisher","unstructured":"Dubslaff C, Baier C, Kl\u00fcppelholz S (2015) Probabilistic model checking for feature-oriented systems. In: Chiba S, Tanter E, Ernst E, Hirschfeld R (eds) Transactions on Aspect-Oriented Software Development XII, LNCS, vol 8989, Springer, pp 180\u2013220. https:\/\/doi.org\/10.1007\/978-3-662-46734-3_5","DOI":"10.1007\/978-3-662-46734-3_5"},{"key":"9930_CR48","doi-asserted-by":"publisher","unstructured":"Fantechi A, Gnesi S (2007) A behavioural model for product families. In: Proceedings of the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT international symposium on foundations of software engineering (ESEC\/FSE07), ACM, pp 521\u2013524. https:\/\/doi.org\/10.1145\/1287624.1287700","DOI":"10.1145\/1287624.1287700"},{"key":"9930_CR49","doi-asserted-by":"publisher","unstructured":"Fantechi A, Gnesi S (2008) Formal modeling for product families engineering. In: Proceedings of the 12th international conference on software product line engineering (SPLC\u201908), IEEE, pp 193\u2013202. https:\/\/doi.org\/10.1109\/SPLC.2008.45","DOI":"10.1109\/SPLC.2008.45"},{"key":"9930_CR50","doi-asserted-by":"publisher","unstructured":"Fischbein D, Uchitel S, Braberman VA (2006) A foundation for behavioural conformance in software product line architectures. In: Proceedings of the ISSTA workshop on role of software architecture for testing and analysis (ROSATEA\u201906), ACM, pp 39\u201348. https:\/\/doi.org\/10.1145\/1147249.1147254","DOI":"10.1145\/1147249.1147254"},{"key":"9930_CR51","doi-asserted-by":"publisher","unstructured":"Gruler A, Leucker M, Scheidemann KD (2008) Modeling and model checking software product lines. In: Barthe G, de Boer FS (eds) Proceedings of the 10th international conference on formal methods for open object-based distributed systems (FMOODS\u201908), LNCS, vol 5051, Springer, pp 113\u2013131. https:\/\/doi.org\/10.1007\/978-3-540-68863-1_8","DOI":"10.1007\/978-3-540-68863-1_8"},{"issue":"3","key":"9930_CR52","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231\u2013274. https:\/\/doi.org\/10.1016\/0167-6423(87)90035-9","journal-title":"Sci Comput Program"},{"key":"9930_CR53","unstructured":"Heule M, J\u00e4rvisalo M, Suda M (2021) The international SAT competitions web page. https:\/\/www.satcompetition.org\/. Accessed 26 June 2021"},{"issue":"8","key":"9930_CR54","doi-asserted-by":"publisher","first-page":"828","DOI":"10.1016\/j.infsof.2012.02.002","volume":"54","author":"G Holl","year":"2012","unstructured":"Holl G, Gr\u00fcnbacher P, Rabiser R (2012) A systematic review and an expert survey on capabilities supporting multi product lines. Inf Softw Technol 54(8):828\u2013852. https:\/\/doi.org\/10.1016\/j.infsof.2012.02.002","journal-title":"Inf Softw Technol"},{"key":"9930_CR55","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2016.09.006","volume":"243","author":"F Hutter","year":"2017","unstructured":"Hutter F, Lindauer M, Balint A, Bayless S, Hoos H, Leyton-Brown K (2017) The configurable SAT solver challenge (CSSC). Artifi Intell 243:1\u201325. https:\/\/doi.org\/10.1016\/j.artint.2016.09.006","journal-title":"Artifi Intell"},{"key":"9930_CR56","doi-asserted-by":"publisher","unstructured":"K\u00e4stner C, Apel S (2008) Type-checking software product lines \u2013 a formal approach. In: Proceedings of the 23rd international conference on automated software engineering (ASE\u201908), IEEE, pp 258\u2013267. https:\/\/doi.org\/10.1109\/ASE.2008.36","DOI":"10.1109\/ASE.2008.36"},{"key":"9930_CR57","doi-asserted-by":"publisher","unstructured":"Kim CHP, Batory DS, Khurshid S (2011) Reducing combinatorics in testing product lines. In: Proceedings of the 10th international conference on aspect-oriented software development (AOSD\u201911), ACM, pp 57\u201368. https:\/\/doi.org\/10.1145\/1960275.1960284","DOI":"10.1145\/1960275.1960284"},{"key":"9930_CR58","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd J (2017) 30 years of modal transition systems: survey of extensions and analysis. In: Aceto L, Bacci G, Bacci G, Ing\u00f3lfsd\u00f3ttir A, Legay A, Mardare R (eds) Models, algorithms, logics and tools, LNCS, vol 10460, Springer, pp 36\u201374. https:\/\/doi.org\/10.1007\/978-3-319-63121-9_3","DOI":"10.1007\/978-3-319-63121-9_3"},{"key":"9930_CR59","doi-asserted-by":"publisher","unstructured":"Larsen KG, Nyman U, W\u0119sowski A (2007) Modal I\/O automata for interface and product line theories. In: De Nicola R (ed) Proceedings of the 16th European symposium on programming (ESOP\u201907), LNCS, vol 4421, Springer, pp 64\u201379. https:\/\/doi.org\/10.1007\/978-3-540-71316-6_6","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"9930_CR60","doi-asserted-by":"publisher","unstructured":"Larsen KG, Thomsen B (1988) A modal process logic. In: Proceedings of the 3rd symposium on logic in computer science (LICS\u201988), IEEE, pp 203\u2013210. https:\/\/doi.org\/10.1109\/LICS.1988.5119","DOI":"10.1109\/LICS.1988.5119"},{"key":"9930_CR61","doi-asserted-by":"publisher","unstructured":"Lauenroth K, Pohl K, T\u00f6hning S (2009) Model checking of domain artifacts in product line engineering. In: Proceedings of the 24th international conference on automated software engineering (ASE\u201909), IEEE, pp 269\u2013280. https:\/\/doi.org\/10.1109\/ASE.2009.16","DOI":"10.1109\/ASE.2009.16"},{"key":"9930_CR62","doi-asserted-by":"publisher","unstructured":"Liang JH, Ganesh V, Czarnecki K, Raman V (2015) SAT-based analysis of large real-world feature models is easy. In: Proceedings of the 19th international software product line conference (SPLC\u201915), ACM, pp 91\u2013100. https:\/\/doi.org\/10.1145\/2791060.2791070","DOI":"10.1145\/2791060.2791070"},{"key":"9930_CR63","doi-asserted-by":"publisher","unstructured":"Lienhardt M, Damiani F, Donetti S, Paolini L (2018a) Multi software product lines in the wild. In: Proceedings of the 12th international workshop on variability modelling of software-intensive systems (VaMoS\u201918), ACM, pp 89\u201396. https:\/\/doi.org\/10.1145\/3168365.3170425","DOI":"10.1145\/3168365.3170425"},{"key":"9930_CR64","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2018.05.007","volume":"166","author":"M Lienhardt","year":"2018","unstructured":"Lienhardt M, Damiani F, Testa L, Turin G (2018b) On checking delta-oriented product lines of statecharts. Sci Comput Program 166:3\u201334. https:\/\/doi.org\/10.1016\/j.scico.2018.05.007","journal-title":"Sci Comput Program"},{"issue":"1","key":"9930_CR65","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/j.jlamp.2015.09.004","volume":"85","author":"M Lochau","year":"2016","unstructured":"Lochau M, Mennicke S, Baller H, Ribbeck L (2016) Incremental model checking of delta-oriented software product lines. J Log Algebr Meth Program 85 (1):245\u2013267. https:\/\/doi.org\/10.1016\/j.jlamp.2015.09.004","journal-title":"J Log Algebr Meth Program"},{"key":"9930_CR66","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-1-4612-4222-2"},{"key":"9930_CR67","unstructured":"Mendonca M, W\u0119sowski A, Czarnecki K (2009) SAT-based analysis of feature models is easy. In: Proceedings of the 13th international software product line conference (SPLC\u201909), ACM, pp 231\u2013240"},{"key":"9930_CR68","doi-asserted-by":"publisher","unstructured":"Nielson F, Nielson HR, Hankin C (2005) Principles of program analysis, Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-662-03811-6","DOI":"10.1007\/978-3-662-03811-6"},{"issue":"4","key":"9930_CR69","doi-asserted-by":"publisher","first-page":"18:1","DOI":"10.1145\/3280986","volume":"27","author":"AV von Rhein","year":"2018","unstructured":"von Rhein AV, Liebig J, Janker A, K\u00e4stner C, Apel S (2018) Variability-aware static analysis at scale: an empirical study. ACM Trans Softw Eng Methodol 27(4):18:1\u201318:33. https:\/\/doi.org\/10.1145\/3280986","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"9930_CR70","doi-asserted-by":"publisher","unstructured":"ter Beek MH, de Vink EP (2014a) Towards modular verification of software product lines with mCRL2. In: Margaria T, Steffen B (eds) Proceedings of the 6th international symposium on leveraging applications of formal methods, verification and validation (ISoLA\u201914), LNCS, vol 8802, Springer, pp 368\u2013385. https:\/\/doi.org\/10.1007\/978-3-662-45234-9_26","DOI":"10.1007\/978-3-662-45234-9_26"},{"key":"9930_CR71","doi-asserted-by":"publisher","unstructured":"ter Beek MH, de Vink EP (2014b) Using mCRL2 for the analysis of software product lines. In: Proceedings of the 2nd FME workshop on formal methods in software engineering (FormaliSE\u201914), IEEE, pp 31\u201337. https:\/\/doi.org\/10.1145\/2593489.2593493","DOI":"10.1145\/2593489.2593493"},{"key":"9930_CR72","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Mazzanti F (2014) VMC: Recent advances and challenges ahead. In: Proceedings of the 18th international software product line conference (SPLC\u201914), vol 2, ACM, pp 70\u201377. https:\/\/doi.org\/10.1145\/2647908.2655969","DOI":"10.1145\/2647908.2655969"},{"key":"9930_CR73","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Mazzanti F, Sulova A (2012) VMC: a tool for product variability analysis. In: Giannakopoulou D, M\u00e9ry D (eds) Proceedings of the 18th international symposium on formal methods (FM\u201912), LNCS, vol 7436, Springer, pp 450\u2013454. https:\/\/doi.org\/10.1007\/978-3-642-32759-9_36","DOI":"10.1007\/978-3-642-32759-9_36"},{"key":"9930_CR74","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Lluch Lafuente A, Petrocchi M (2013) Combining declarative and procedural views in the specification and analysis of product families. In: Proceedings of the 17th international software product line conference (SPLC\u201913), vol 2, ACM, pp 10\u201317. https:\/\/doi.org\/10.1145\/2499777.2500722","DOI":"10.1145\/2499777.2500722"},{"key":"9930_CR75","doi-asserted-by":"publisher","unstructured":"ter Beek M, Damiani F, Gnesi S, Mazzanti F, Paolini L (2015a) From featured transition systems to modal transition systems with variability constraints. In: Calinescu R, Rumpe B (eds) Proceedings of the 13th international conference on software engineering and formal methods (SEFM\u201915), LNCS, vol 9276, Springer, pp 344\u2013359. https:\/\/doi.org\/10.1007\/978-3-319-22969-0_24","DOI":"10.1007\/978-3-319-22969-0_24"},{"key":"9930_CR76","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2015b) Using FMC for family-based analysis of software product lines. In: Proceedings of the 19th international software product line conference (SPLC\u201915), ACM, pp 432\u2013439. https:\/\/doi.org\/10.1145\/2791060.2791118","DOI":"10.1145\/2791060.2791118"},{"key":"9930_CR77","doi-asserted-by":"publisher","first-page":"56","DOI":"10.4204\/EPTCS.182.5","volume":"182","author":"MH ter Beek","year":"2015","unstructured":"ter Beek MH, Legay A, Lluch Lafuente A, Vandin A (2015c) Quantitative analysis of probabilistic models of software product lines with statistical model checking. Electron Proc Theor Comput Sci 182:56\u201370. https:\/\/doi.org\/10.4204\/EPTCS.182.5","journal-title":"Electron Proc Theor Comput Sci"},{"issue":"2","key":"9930_CR78","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.jlamp.2015.11.006","volume":"85","author":"MH ter Beek","year":"2016","unstructured":"ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2016a) Modelling and analysing variability in product families: Model checking of modal transition systems with variability constraints. J Log Algebr Meth Program 85(2):287\u2013315. https:\/\/doi.org\/10.1016\/j.jlamp.2015.11.006","journal-title":"J Log Algebr Meth Program"},{"key":"9930_CR79","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Reniers MA, de Vink EP (2016b) Supervisory controller synthesis for product lines using CIF 3. In: Margaria T, Steffen B (eds) Proceedings of the 7th international symposium on leveraging applications of formal methods, verification and validation: foundational techniques (ISoLA\u201916), LNCS, vol 9952, Springer, pp 856\u2013873. https:\/\/doi.org\/10.1007\/978-3-319-47166-2_59","DOI":"10.1007\/978-3-319-47166-2_59"},{"key":"9930_CR80","doi-asserted-by":"publisher","unstructured":"ter Beek M, de Vink EP, Willemse TAC (2017) Family-based model checking with mCRL2. In: Huisman M, Rubin J (eds) Proceedings of the 20th international conference on fundamental approaches to software engineering (FASE\u201917), LNCS, vol 10202, Springer, pp 387\u2013405. https:\/\/doi.org\/10.1007\/978-3-662-54494-5_23","DOI":"10.1007\/978-3-662-54494-5_23"},{"key":"9930_CR81","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Damiani F, Lienhardt M, Mazzanti F, Paolini L (2019a) Static analysis of featured transition systems. In: Proceedings of the 23rd international systems and software product line conference (SPLC\u201919), ACM, pp 39\u201351. https:\/\/doi.org\/10.1145\/3336294.3336295","DOI":"10.1145\/3336294.3336295"},{"key":"9930_CR82","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2018.09.006","volume":"169","author":"MH ter Beek","year":"2019","unstructured":"ter Beek MH, Damiani F, Gnesi S, Mazzanti F, Paolini L (2019b) On the expressiveness of modal transition systems with variability constraints. Sci Comput Program 169:1\u201317. https:\/\/doi.org\/10.1016\/j.scico.2018.09.006","journal-title":"Sci Comput Program"},{"key":"9930_CR83","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Damiani F, Lienhardt M, Mazzanti F, Paolini L (2019c) Supplementary material for: \u201cStatic analysis of featured transition systems\u201d. https:\/\/doi.org\/10.5281\/zenodo.2616646","DOI":"10.5281\/zenodo.2616646"},{"key":"9930_CR84","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2019d) States and events in KandISTI: a retrospective. In: Margaria T, Graf S, Larsen KG (eds) Models, mindsets, meta: the what, the how, and the why not?, LNCS, vol 11200, Springer, pp 110\u2013128. https:\/\/doi.org\/10.1007\/978-3-030-22348-9_9","DOI":"10.1007\/978-3-030-22348-9_9"},{"issue":"3","key":"9930_CR85","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1109\/TSE.2018.2853726","volume":"46","author":"MH ter Beek","year":"2020","unstructured":"ter Beek MH, Legay A, Lluch Lafuente A, Vandin A (2020a) A framework for quantitative modeling and analysis of highly (re)configurable systems. IEEE Trans Softw Eng 46(3):321\u2013345. https:\/\/doi.org\/10.1109\/TSE.2018.2853726","journal-title":"IEEE Trans Softw Eng"},{"key":"9930_CR86","doi-asserted-by":"publisher","unstructured":"ter Beek MH, van Loo S, de Vink EP, Willemse TAC (2020b) Family-based SPL model checking using parity games with variability. In: Wehrheim H, Cabot J (eds) Proceedings of the 23rd international conference on fundamental approaches to software engineering (FASE\u201920), LNCS, vol 12076, Springer, pp 245\u2013265. https:\/\/doi.org\/10.1007\/978-3-030-45234-6_12","DOI":"10.1007\/978-3-030-45234-6_12"},{"key":"9930_CR87","doi-asserted-by":"publisher","unstructured":"ter Beek MH, Mazzanti F, Damiani F, Paolini L, Scarso G, Valfr\u00e8 M, Lienhardt L (2021) Static analysis and family-based model checking of featured transition systems with VMC. In: Proceedings of the 25th international systems and software product line conference (SPLC\u201921), ACM. pp 24\u201327 https:\/\/doi.org\/10.1145\/3461002.3473071","DOI":"10.1145\/3461002.3473071"},{"issue":"1","key":"9930_CR88","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2580950","volume":"47","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm T, Apel S, K\u00e4stner C, Schaefer I, Saake G (2014) A classification and survey of analysis strategies for software product lines. ACM Comput Surv 47(1):6:1\u20136:45. https:\/\/doi.org\/10.1145\/2580950","journal-title":"ACM Comput Surv"},{"key":"9930_CR89","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.scico.2012.06.002","volume":"79","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm T., K\u00e4stner C., Benduhn F, Meinicke J, Saake G, Leich T (2014) FeatureIDE: An extensible framework for feature-oriented software development. Sci Comput Program 79:70\u201385. https:\/\/doi.org\/10.1016\/j.scico.2012.06.002","journal-title":"Sci Comput Program"},{"key":"9930_CR90","doi-asserted-by":"publisher","unstructured":"Vandin A, ter Beek MH, Legay A, Lluch Lafuente A (2018) QFLan: a tool for the quantitative analysis of highly reconfigurable systems. In: Havelund K, Peleska J, Roscoe B, de Vink E (eds) Proceedings of the 22nd international symposium on formal methods (FM\u201918), LNCS. https:\/\/doi.org\/10.1007\/978-3-319-95582-7_19, vol 10951. Springer, pp 329\u2013337","DOI":"10.1007\/978-3-319-95582-7_19"},{"key":"9930_CR91","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/j.scico.2018.09.001","volume":"168","author":"M Varshosaz","year":"2018","unstructured":"Varshosaz M, Beohar H, Mousavi MR (2018) Basic behavioral models for software product lines: Revisited. Sci Comput Program 168:171\u2013185. https:\/\/doi.org\/10.1016\/j.scico.2018.09.001","journal-title":"Sci Comput Program"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-020-09930-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10664-020-09930-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-020-09930-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T08:08:49Z","timestamp":1643184529000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10664-020-09930-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,23]]},"references-count":91,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,1]]}},"alternative-id":["9930"],"URL":"https:\/\/doi.org\/10.1007\/s10664-020-09930-8","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,23]]},"assertion":[{"value":"17 December 2020","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 October 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"10"}}