{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:44:38Z","timestamp":1742917478935,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030309848"},{"type":"electronic","value":"9783030309855"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30985-5_19","type":"book-chapter","created":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T17:53:39Z","timestamp":1570557219000},"page":"313-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Product Line Verification via Modal Meta Model Checking"],"prefix":"10.1007","author":[{"given":"Tim","family":"Tegeler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alnis","family":"Murtovi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Frohme","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,9]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"Asirelli, P., ter Beek, M.H., Gnesi, S., Fantechi, A.: Formal description of variability in product families. In: 2011 15th International Software Product Line Conference, pp. 130\u2013139, August 2011. \n                      https:\/\/doi.org\/10.1109\/SPLC.2011.34","DOI":"10.1109\/SPLC.2011.34"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-16265-7_5","volume-title":"Integrated Formal Methods","author":"P Asirelli","year":"2010","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A logical framework to deal with variability. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 43\u201358. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-16265-7_5"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-21461-5_3","volume-title":"Formal Techniques for Distributed Systems","author":"P Asirelli","year":"2011","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A model-checking tool for families of services. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE -2011. LNCS, vol. 6722, pp. 44\u201358. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-21461-5_3"},{"issue":"2","key":"19_CR4","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.jlamp.2015.11.006","volume":"85","author":"MH Beek ter","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. Algebraic Methods Program. 85(2), 287\u2013315 (2016). \n                      https:\/\/doi.org\/10.1016\/j.jlamp.2015.11.006","journal-title":"J. Log. Algebraic Methods Program."},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: States and events in KandISTI. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not? LNCS, vol. 11200, pp. 110\u2013128. Springer, Cham (2019). \n                      https:\/\/doi.org\/10.1007\/978-3-030-22348-9_8","DOI":"10.1007\/978-3-030-22348-9_8"},{"key":"19_CR6","unstructured":"Bertolino, A., Fantechi, A., Gnesi, S., Lami, G., Maccari, A.: Use case description of requirements for product lines. In: Proceedings of the International Workshop on Requirements Engineering for Product Lines 2002 - REPL 2002. Technical report: ALR2002-033, AVAYA, pp. 12\u201318 (2002)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-24667-1_14","volume-title":"Software Product-Family Engineering","author":"A Bertolino","year":"2004","unstructured":"Bertolino, A., Gnesi, S.: PLUTO: a test methodology for product families. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 181\u2013197. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24667-1_14"},{"key":"19_CR8","series-title":"Studies in Logic and Practical Reasoning","volume-title":"Handbook of Modal Logic","author":"P Blackburn","year":"2006","unstructured":"Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier Science Inc., New York (2006)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"CONCUR 1992","author":"O Burkart","year":"1992","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123\u2013137. Springer, Heidelberg (1992). \n                      https:\/\/doi.org\/10.1007\/BFb0084787"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-540-48654-1_9","volume-title":"CONCUR 1994: Concurrency Theory","author":"O Burkart","year":"1994","unstructured":"Burkart, O., Steffen, B.: Pushdown processes: parallel composition and model checking. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 98\u2013113. Springer, Heidelberg (1994). \n                      https:\/\/doi.org\/10.1007\/978-3-540-48654-1_9"},{"issue":"1\u20132","key":"19_CR11","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0304-3975(99)00034-1","volume":"221","author":"O Burkart","year":"1999","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theor. Comput. Sci. 221(1\u20132), 251\u2013270 (1999). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(99)00034-1","journal-title":"Theor. Comput. Sci."},{"key":"19_CR12","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"5","key":"19_CR13","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, P.Y.: Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transfer 14(5), 589\u2013612 (2012). \n                      https:\/\/doi.org\/10.1007\/s10009-012-0234-1","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"8","key":"19_CR14","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, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Software Eng. 39(8), 1069\u20131089 (2013). \n                      https:\/\/doi.org\/10.1109\/TSE.2012.86","journal-title":"IEEE Trans. Software Eng."},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering, ICSE 2010, vol. 1, pp. 335\u2013344. ACM, New York (2010). \n                      https:\/\/doi.org\/10.1145\/1806799.1806850","DOI":"10.1145\/1806799.1806850"},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Methods Syst. Des. 2(2), 121\u2013147 (1993). \n                      https:\/\/doi.org\/10.1007\/BF01383878","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Model checking and the mu-calculus. In: DIMACS Series in Discrete Mathematics, pp. 185\u2013214. American Mathematical Society (1997)","DOI":"10.1090\/dimacs\/031\/06"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Fantechi, A., Gnesi, S.: Formal modeling for product families engineering. In: 2008 12th International Software Product Line Conference, pp. 193\u2013202, September 2008. \n                      https:\/\/doi.org\/10.1109\/SPLC.2008.45","DOI":"10.1109\/SPLC.2008.45"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-030-00244-2_10","volume-title":"Formal Methods for Industrial Critical Systems","author":"M Frohme","year":"2018","unstructured":"Frohme, M., Steffen, B.: Active mining of document type definitions. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 147\u2013161. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-00244-2_10"},{"key":"19_CR20","unstructured":"Frohme, M., Steffen, B.: Compositional Learning of Mutually Recursive Procedural Systems (2018, under submission)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-030-00244-2_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"H Garavel","year":"2018","unstructured":"Garavel, H., Lang, F., Mounier, L.: Compositional verification in action. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 189\u2013210. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-00244-2_13"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/BFb0023732","volume-title":"Computer-Aided Verification","author":"S Graf","year":"1991","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186\u2013196. Springer, Heidelberg (1991). \n                      https:\/\/doi.org\/10.1007\/BFb0023732"},{"issue":"5","key":"19_CR24","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S Graf","year":"1996","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Aspects Comput. 8(5), 607\u2013616 (1996). \n                      https:\/\/doi.org\/10.1007\/BF01211911","journal-title":"Formal Aspects Comput."},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science, pp. 203\u2013210. IEEE (1988). \n                      https:\/\/doi.org\/10.1109\/LICS.1988.5119","DOI":"10.1109\/LICS.1988.5119"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232\u2013246. Springer, Heidelberg (1990). \n                      https:\/\/doi.org\/10.1007\/3-540-52148-8_19"},{"issue":"1","key":"19_CR27","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11\u201344 (1995). \n                      https:\/\/doi.org\/10.1007\/BF01384313","journal-title":"Formal Methods Syst. Des."},{"issue":"6","key":"19_CR28","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1109\/MC.2010.177","volume":"43","author":"T Margaria","year":"2010","unstructured":"Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. IEEE Comput. 43(6), 90\u201392 (2010). \n                      https:\/\/doi.org\/10.1109\/MC.2010.177","journal-title":"IEEE Comput."},{"issue":"3","key":"19_CR29","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10009-017-0453-6","volume":"20","author":"S Naujokat","year":"2018","unstructured":"Naujokat, S., Lybecait, M., Kopetzki, D., Steffen, B.: CINCO: a simplicity-driven approach to full generation of domain-specific graphical modeling tools. STTT 20(3), 327\u2013354 (2018). \n                      https:\/\/doi.org\/10.1007\/s10009-017-0453-6","journal-title":"STTT"},{"key":"19_CR30","doi-asserted-by":"publisher","unstructured":"O\u2019Connor, R., Elger, P., Clarke, P.: Continuous software engineering\u2014a microservices architecture perspective. J. Softw. Evol. Process 29 (2017). \n                      https:\/\/doi.org\/10.1002\/smr.1866","DOI":"10.1002\/smr.1866"},{"key":"19_CR31","series-title":"Foundations Principles and Techniques","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering","author":"K Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.J.: Software Product Line Engineering. Foundations Principles and Techniques. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/3-540-28901-1"},{"key":"19_CR32","unstructured":"Shahin, M., Babar, M.A., Zhu, L.: Continuous integration, delivery and deployment: a systematic review on approaches, tools, challenges and practices. CoRR abs\/1703.07019 (2017). \n                      http:\/\/arxiv.org\/abs\/1703.07019"},{"key":"19_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346\u2013364. Springer, Heidelberg (1991). \n                      https:\/\/doi.org\/10.1007\/3-540-54415-1_54"},{"issue":"2","key":"19_CR34","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0167-6423(93)90003-8","volume":"21","author":"B Steffen","year":"1993","unstructured":"Steffen, B.: Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115\u2013139 (1993). \n                      https:\/\/doi.org\/10.1016\/0167-6423(93)90003-8","journal-title":"Sci. Comput. Program."},{"key":"19_CR35","unstructured":"Steffen, B.: Method for Incremental Synthesis of a Discrete Technical System (1998). \n                      https:\/\/patents.google.com\/patent\/WO1998024022A1\/en"},{"key":"19_CR36","unstructured":"Steffen, B., Gossen, F., Naujokat, S., Margaria, T.: Language-driven engineering: from general-purpose to purpose-specific languages. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science: State of the Art and Perspectives, LNCS, vol. 10000. Springer (2018). \n                      https:\/\/www.springer.com\/gp\/book\/9783319919072"},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-00244-2_15","volume-title":"Formal Methods for Industrial Critical Systems","author":"B Steffen","year":"2018","unstructured":"Steffen, B., Murtovi, A.: M3C: modal meta model checking. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 223\u2013241. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-00244-2_15"},{"key":"19_CR38","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-46508-1_3","volume":"1","author":"B Steffen","year":"2016","unstructured":"Steffen, B., Naujokat, S.: Archimedean points: the essence for mastering change. Trans. Found. Mastering Chang. 1, 22\u201346 (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46508-1_3","journal-title":"Trans. Found. Mastering Chang."}],"container-title":["Lecture Notes in Computer Science","From Software Engineering to Formal Methods and Tools, and Back"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30985-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T06:53:29Z","timestamp":1570604009000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30985-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309848","9783030309855"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30985-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"9 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}