{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T16:57:38Z","timestamp":1772038658171,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544938","type":"print"},{"value":"9783662544945","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54494-5_23","type":"book-chapter","created":{"date-parts":[[2017,3,22]],"date-time":"2017-03-22T00:09:02Z","timestamp":1490141342000},"page":"387-405","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Family-Based Model Checking with mCRL2"],"prefix":"10.1007","author":[{"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"given":"Erik P.","family":"de Vink","sequence":"additional","affiliation":[]},{"given":"Tim A. C.","family":"Willemse","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,22]]},"reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2580950","volume":"47","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm, T., et al.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 1\u201345 (2014)","journal-title":"ACM Comput. Surv."},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-68863-1_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"A Gruler","year":"2008","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113\u2013131. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-68863-1_8"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Lauenroth, K., Pohl, K., T\u00f6hning, S.: Model checking of domain artifacts in product line engineering. In: ASE, pp. 269\u2013280. IEEE (2009)","DOI":"10.1109\/ASE.2009.16"},{"key":"23_CR4","unstructured":"Classen, A., et al.: Model checking $$\\underline{\\text{lots}}$$ of systems: efficient verification of temporal properties in software product lines. In: ICSE, pp. 335\u2013344. ACM (2010)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-34026-0_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"F Damiani","year":"2012","unstructured":"Damiani, F., Schaefer, I.: Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 193\u2013207. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-34026-0_15"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: GPCE, pp. 11\u201320. ACM (2012)","DOI":"10.1145\/2371401.2371404"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: SPLC, pp. 432\u2013439. ACM (2015)","DOI":"10.1145\/2791060.2791118"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-319-23404-5_18","volume-title":"Model Checking Software","author":"AS Dimovski","year":"2015","unstructured":"Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., W\u0105sowski, A.: Family-based model checking without a family-based model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282\u2013299. Springer, Cham (2015). doi:10.1007\/978-3-319-23404-5_18"},{"issue":"11","key":"23_CR9","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. C. ACM 52(11), 74\u201384 (2009)","journal-title":"C. ACM"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Calculating and modeling common parts of software product lines. In: SPLC, pp. 203\u2013212. IEEE (2008)","DOI":"10.1109\/SPLC.2008.22"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Lluch Lafuente, A., Petrocchi, M.: Combining declarative and procedural views in the specification and analysis of product families. In: SPLC, vol. 2, pp. 10\u201317. ACM (2013)","DOI":"10.1145\/2499777.2500722"},{"issue":"1","key":"23_CR12","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.: Incremental model checking delta-oriented software product lines. J. Log. Algebr. Meth. Program. 85(1), 245\u2013267 (2016)","journal-title":"J. Log. Algebr. Meth. Program."},{"issue":"8","key":"23_CR13","doi-asserted-by":"publisher","first-page":"1069","DOI":"10.1109\/TSE.2012.86","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen, A., et al.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069\u20131089 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"B","key":"23_CR14","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., et al.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80(B), 416\u2013439 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"23_CR15","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, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: 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 (2016)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-32759-9_36","volume-title":"FM 2012: Formal Methods","author":"MH ter Beek","year":"2012","unstructured":"ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450\u2013454. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-32759-9_36"},{"issue":"5","key":"23_CR17","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-012-0234-1","volume":"14","author":"A Classen","year":"2012","unstructured":"Classen, A., et al.: Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf. 14(5), 589\u2013612 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Cordy, A., et al.: ProVeLines: a product line of verifiers for software product lines. In: SPLC, vol. 2, pp. 141\u2013146. ACM (2013)","DOI":"10.1145\/2499777.2499781"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink, E.P.: Using mCRL2 for the analysis of software product lines. In: FormaliSE, pp. 31\u201337. IEEE (2014)","DOI":"10.1145\/2593489.2593493"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Towards a feature mu-calculus targeting SPL verification. In: FMSPLE, EPTCS, vol. 206, pp. 61\u201375 (2016)","DOI":"10.4204\/EPTCS.206.6"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-36742-7_15"},{"key":"23_CR22","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Kim, C.H.P., et al.: SPLat: lightweight dynamic analysis for reducing combinatorics in testing configurable systems. In: ESEC\/FSE, pp. 257\u2013267. ACM (2013)","DOI":"10.1145\/2491411.2491459"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-662-46675-9_6","volume-title":"Fundamental Approaches to Software Engineering","author":"J B\u00fcrdek","year":"2015","unstructured":"B\u00fcrdek, J., Lochau, M., Bauregger, S., Holzer, A., von Rhein, A., Apel, S., Beyer, D.: Facilitating reuse in multi-goal test-suite generation for software product lines. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 84\u201399. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46675-9_6"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-35122-3_1","volume-title":"Software Reuse: Bridging with Social-Awareness","author":"S Lity","year":"2016","unstructured":"Lity, S., Morbach, T., Th\u00fcm, T., Schaefer, I.: Applying incremental model slicing to product-line regression testing. In: Kapitsaki, G.M., Santana de Almeida, E. (eds.) ICSR 2016. LNCS, vol. 9679, pp. 3\u201319. Springer, Cham (2016). doi:10.1007\/978-3-319-35122-3_1"},{"key":"23_CR26","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, M.R.: Basic behavioral models for software product lines: expressiveness and testing pre-orders. Sci. Comput. Program. 123, 42\u201360 (2016)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"23_CR27","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1016\/j.infsof.2012.07.017","volume":"55","author":"C Ghezzi","year":"2013","unstructured":"Ghezzi, C., Sharifloo, A.: Model-based verification of quantitative non-functional properties for software product lines. Inform. Softw. Technol. 55(3), 508\u2013524 (2013)","journal-title":"Inform. Softw. Technol."},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Varshosaz, M., Khosravi, R.: Discrete time markov chain families: modeling and verification of probabilistic software product lines. In: SPLC, vol. 2, pp. 34\u201341. ACM (2013)","DOI":"10.1145\/2499777.2500725"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Rodrigues, G.N., et al.: Modeling and verification for probabilistic properties in software product lines. In: HASE, pp. 173\u2013180. IEEE (2015)","DOI":"10.1109\/HASE.2015.34"},{"key":"23_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-662-46734-3_5","volume-title":"Transactions on Aspect-Oriented Software Development XII","author":"C Dubslaff","year":"2015","unstructured":"Dubslaff, C., Baier, C., Kl\u00fcppelholz, S.: Probabilistic model checking for feature-oriented systems. In: Chiba, S., Tanter, \u00c9., Ernst, E., Hirschfeld, R. (eds.) Transactions on Aspect-Oriented Software Development XII. LNCS, vol. 8989, pp. 180\u2013220. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46734-3_5"},{"key":"23_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22110-1_47"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-662-49665-7_17","volume-title":"Fundamental Approaches to Software Engineering","author":"P Chrszon","year":"2016","unstructured":"Chrszon, P., Dubslaff, C., Kl\u00fcppelholz, S., Baier, C.: Family-based modeling and analysis for probabilistic systems \u2013 featuring ProFeat. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 287\u2013304. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49665-7_17"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: SPLC, pp. 11\u201315. ACM (2015)","DOI":"10.1145\/2791060.2791087"},{"key":"23_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-47166-2_8","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"MH ter Beek","year":"2016","unstructured":"ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114\u2013133. Springer, Cham (2016). doi:10.1007\/978-3-319-47166-2_8"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Bradfield, J.C., Stirling, C.: Modal logics and $$\\mu $$-calculi: an introduction. In: Handbook of Process Algebra, Chap. 4, pp. 293\u2013330. Elsevier (2001)","DOI":"10.1016\/B978-044482830-9\/50022-9"},{"key":"23_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49253-4_8","volume-title":"Algebraic Methodology and Software Technology","author":"JF Groote","year":"1998","unstructured":"Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: Haeberer, A.M. (ed.) AMAST 1999. LNCS, vol. 1548, pp. 74\u201390. Springer, Heidelberg (1998). doi:10.1007\/3-540-49253-4_8"},{"issue":"3","key":"23_CR37","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.scico.2004.08.002","volume":"56","author":"JF Groote","year":"2005","unstructured":"Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Sci. Comput. Program. 56(3), 251\u2013273 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"1\u20132","key":"23_CR38","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/S1567-8326(01)00013-3","volume":"49","author":"H Zantema","year":"2001","unstructured":"Zantema, H., van de Pol, J.C.: A rewriting approach to binary decision diagrams. J. Log. Algebr. Program. 49(1\u20132), 61\u201386 (2001)","journal-title":"J. Log. Algebr. Program."},{"issue":"1","key":"23_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1049\/ip-d.1983.0001","volume":"130","author":"J Kramer","year":"1983","unstructured":"Kramer, J., Magee, J., Sloman, M., Lister, A.: CONIC: an integrated approach to distributed computer control systems. IEE Proc. E 130(1), 1\u201310 (1983)","journal-title":"IEE Proc. E"},{"key":"23_CR40","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: ESEC\/FSE, pp. 257\u2013266. ACM (2003)","DOI":"10.1145\/949952.940106"},{"key":"23_CR41","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54494-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:26:02Z","timestamp":1618971962000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54494-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544938","9783662544945"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54494-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"22 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}