{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T03:10:28Z","timestamp":1770347428615,"version":"3.49.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319155449","type":"print"},{"value":"9783319155456","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15545-6_20","type":"book-chapter","created":{"date-parts":[[2015,3,5]],"date-time":"2015-03-05T02:19:15Z","timestamp":1425521955000},"page":"312-328","source":"Crossref","is-referenced-by-count":14,"title":["From EU Projects to a Family of Model Checkers"],"prefix":"10.1007","author":[{"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[]},{"given":"Franco","family":"Mazzanti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-02138-1_15","volume-title":"Formal Techniques for Distributed Systems","author":"J. Abreu","year":"2009","unstructured":"Abreu, J., Mazzanti, F., Fiadeiro, J.L., Gnesi, S.: A Model-Checking Approach for Service Component Architectures. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol.\u00a05522, pp. 219\u2013224. Springer, Heidelberg (2009)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-40020-2_1","volume-title":"Recent Trends in Algebraic Development Techniques","author":"L. Andrade","year":"2003","unstructured":"Andrade, L., et al.: AGILE: Software Architecture for Mobility. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol.\u00a02755, pp. 1\u201333. Springer, Heidelberg (2003)"},{"key":"20_CR3","first-page":"94","volume":"95","author":"A. Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., W\u0105sowski, A.: 20 Years of Modal and Mixed Specifications. Bulletin of the EATCS\u00a095, 94\u2013129 (2008)","journal-title":"Bulletin of the EATCS"},{"key":"20_CR4","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.) FORTE 2011 and FMOODS 2011. LNCS, vol.\u00a06722, pp. 44\u201358. Springer, Heidelberg (2011)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: Formal Description of Variability in Product Families. In: SPLC, pp. 130\u2013139. IEEE (2011)","DOI":"10.1109\/SPLC.2011.34"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A Compositional Framework to Derive Product Line Behavioural Descriptions. In: [49], pp. 146\u2013161","DOI":"10.1007\/978-3-642-34026-0_12"},{"key":"20_CR7","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H.: Sensoria Results Applied to the Case Studies. In: [57], pp. 655\u2013677","DOI":"10.1007\/978-3-642-20401-2_32"},{"key":"20_CR9","first-page":"32","volume":"98","author":"M.H. Beek ter","year":"2014","unstructured":"ter Beek, M.H., Bortolussi, L., Ciancia, V., Gnesi, S., Hillston, J., Latella, D., Massink, M.: A Quantitative Approach to the Design and Analysis of Collective Adaptive Systems for Smart Cities. ERCIM News: Smart Cities\u00a098, 32 (2014)","journal-title":"ERCIM News: Smart Cities"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink, E.P.: Software Product Line Analysis with mCRL2. In: [38], pp. 78\u201385","DOI":"10.1145\/2647908.2655970"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., de Vink, E.P.: Towards Modular Verification of Software Product Lines with mCRL2. In: [50], pp. 368\u2013385","DOI":"10.1007\/978-3-662-45234-9_26"},{"key":"20_CR12","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":"20_CR13","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S.: Challenges in Modelling and Analyzing Quantitative Aspects of Bike-Sharing Systems. In: [50], pp. 351\u2013367","DOI":"10.1007\/978-3-662-45234-9_25"},{"issue":"2","key":"20_CR14","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"M.H. Beek ter","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Science of Computer Programming\u00a076(2), 119\u2013135 (2011)","journal-title":"Science of Computer Programming"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Gnesi, S., Koch, N., Mazzanti, F.: Formal verification of an automotive scenario in service-oriented computing. In: ICSE, pp. 613\u2013622. ACM (2008)","DOI":"10.1145\/1368088.1368173"},{"key":"20_CR16","first-page":"50","volume":"93","author":"M.H. Beek ter","year":"2013","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F.: VMC: A Tool for the Analysis of Variability in Software Product Lines. ERCIM News: Mobile Computing\u00a093, 50\u201351 (2013)","journal-title":"ERCIM News: Mobile Computing"},{"key":"20_CR17","first-page":"31","volume":"99","author":"M.H. Beek ter","year":"2014","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F.: KandISTI: A Family of Model Checkers for the Analysis of Software Designs. ERCIM News: Software Quality\u00a099, 31\u201332 (2014)","journal-title":"ERCIM News: Software Quality"},{"key":"20_CR18","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F.: Model Checking Value-Passing Modal Specifications. In: PSI. LNCS, Springer (to appear, 2014)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Gnesi, S., Mazzanti, F., Moiso, C.: Formal Modelling and Verification of an Asynchronous Extension of SOAP. In: ECOWS, pp. 287\u2013296. IEEE (2006)","DOI":"10.1109\/ECOWS.2006.22"},{"key":"20_CR20","unstructured":"ter Beek, M.H., Gnesi, S., Montangero, C., Semini, L.: Detecting policy conflicts by model checking UML state machines. In: ICFI, pp. 59\u201374. IOS Press (2009)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Lapadula, A., Loreti, M., Palasciano, C.: Analysing Robot Movement Using the Sensoria Methods. In: [57], pp. 678\u2013697","DOI":"10.1007\/978-3-642-20401-2_33"},{"key":"20_CR22","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.\u00a02, pp. 10\u201317. ACM (2013)","DOI":"10.1145\/2499777.2500722"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Mazzanti, F.: VMC: Recent Advances and Challenges Ahead. In: [38], pp. 70\u201377","DOI":"10.1145\/2647908.2655969"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Mazzanti, F., Gnesi, S.: CMC\u2013UMC: a framework for the verification of abstract service-oriented properties. In: SAC, pp. 2111\u20132117. ACM (2009)","DOI":"10.1145\/1529282.1529751"},{"key":"20_CR25","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":"M.H. Beek ter","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.\u00a07436, pp. 450\u2013454. Springer, Heidelberg (2012)"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Benavides, D., Segura, S., Ruiz-Cort\u00e9s, A.: Automated Analysis of Feature Models 20 Years Later: a Literature Review. Information Systems\u00a035(6) (2010)","DOI":"10.1016\/j.is.2010.01.001"},{"key":"20_CR27","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"issue":"B","key":"20_CR28","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, P.-Y.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Science of Computer Programming\u00a080(B), 416\u2013439 (2014)","journal-title":"Science of Computer Programming"},{"issue":"8","key":"20_CR29","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 Transactions on Software Engineering\u00a039(8), 1069\u20131089 (2013)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"20_CR30","unstructured":"Clements, P.C., Northrop, L.M.: Software Product Lines: Practices and Patterns. Addison-Wesley (2002)"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","year":"2007","unstructured":"De Nicola, R. (ed.): ESOP 2007. LNCS, vol.\u00a04421. Springer, Heidelberg (2007)"},{"key":"20_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R. De Nicola","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.W.: Action versus State based Logics for Transition Systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol.\u00a0469, pp. 407\u2013419. Springer, Heidelberg (1990)"},{"issue":"2","key":"20_CR33","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. De Nicola","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. Journal of the ACM\u00a042(2), 458\u2013487 (1995)","journal-title":"Journal of the ACM"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Fantechi, A., Gnesi, S.: A behavioural model for product families. In: ESEC\/FSE, pp. 521\u2013524. ACM (2007)","DOI":"10.1145\/1295014.1295031"},{"issue":"3","key":"20_CR35","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/2211616.2211619","volume":"21","author":"A. Fantechi","year":"2012","unstructured":"Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A logical verification methodology for service-oriented computing. ACM Transactions on Software Engineering and Methodology\u00a021(3), 16 (2012)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"20_CR36","unstructured":"Fidge, C.: A Comparative Introduction to CSP, CCS and LOTOS. Technical Report 93-24, Software Verification Research Centre, University of Queensland (January 1994)"},{"key":"20_CR37","doi-asserted-by":"crossref","unstructured":"Fischbein, D., Uchitel, S., Braberman, V.A.: A foundation for behavioural conformance in software product line architectures. In: ROSATEA, pp. 39\u201348. ACM (2006)","DOI":"10.1145\/1147249.1147254"},{"key":"20_CR38","unstructured":"Gnesi, S., Fantechi, A., ter Beek, M.H., Botterweck, G., Becker, M.: Proceedings of the 18th International Software Product Line Conference (SPLC 2014), vol.\u00a02. ACM (2014)"},{"key":"20_CR39","unstructured":"Gnesi, S., Mazzanti, F.: On the Fly Verification of Networks of Automata. In: PDPTA, pp. 1040\u20131046. CSREA Press (1999)"},{"key":"20_CR40","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Mazzanti, F.: An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems. In: [57], pp. 390\u2013407","DOI":"10.1007\/978-3-642-20401-2_18"},{"key":"20_CR41","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Petrocchi, M.: Towards an executable algebra for product lines. In: SPLC, vol.\u00a02, pp. 66\u201373. ACM (2012)","DOI":"10.1145\/2364412.2364424"},{"key":"20_CR42","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., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 113\u2013131. Springer, Heidelberg (2008)"},{"key":"20_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-540-45221-8_33","volume-title":"\u00abUML\u00bb 2003 - The Unified Modeling Language. Modeling Languages and Applications","author":"\u00d8. Haugen","year":"2003","unstructured":"Haugen, \u00d8., St\u00f8len, K.: STAIRS \u2013 Steps To Analyze Interactions with Refinement Semantics. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol.\u00a02863, pp. 388\u2013402. Springer, Heidelberg (2003)"},{"key":"20_CR44","doi-asserted-by":"crossref","unstructured":"Lapadula, A., Pugliese, R., Tiezzi, F.: A Calculus for Orchestration of Web Services. In: [31], pp. 33\u201347","DOI":"10.1007\/978-3-540-71316-6_4"},{"key":"20_CR45","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: Modal I\/O Automata for Interface and Product Line Theories. In: [31], pp. 64\u201379","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"20_CR46","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":"20_CR47","doi-asserted-by":"crossref","unstructured":"Leucker, M., Thoma, D.: A Formal Approach to Software Product Families. In: [49], pp. 131\u2013145","DOI":"10.1007\/978-3-642-34026-0_11"},{"key":"20_CR48","doi-asserted-by":"crossref","unstructured":"Lochau, M., Mennicke, S., Baller, H., Ribbeck, L.: DeltaCCS: A Core Calculus for Behavioral Change. In: [50], pp. 320\u2013335","DOI":"10.1007\/978-3-662-45234-9_23"},{"key":"20_CR49","series-title":"Lecture Notes in Computer Science","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","year":"2012","unstructured":"Margaria, T., Steffen, B. (eds.): ISoLA 2012, Part I. LNCS, vol.\u00a07609. Springer, Heidelberg (2012)"},{"key":"20_CR50","series-title":"Lecture Notes in Computer Science","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","year":"2014","unstructured":"Margaria, T., Steffen, B. (eds.): ISoLA 2014, Part I. LNCS, vol.\u00a08802. Springer, Heidelberg (2014)"},{"key":"20_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/978-3-319-10702-8_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"F. Mazzanti","year":"2014","unstructured":"Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A.: Deadlock Avoidance in Train Scheduling: A Model Checking Approach. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol.\u00a08718, pp. 109\u2013123. Springer, Heidelberg (2014)"},{"key":"20_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-319-06200-6_22","volume-title":"NASA Formal Methods","author":"F. Mazzanti","year":"2014","unstructured":"Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Designing a Deadlock-Free Train Scheduler: A Model Checking Approach. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol.\u00a08430, pp. 264\u2013269. Springer, Heidelberg (2014)"},{"key":"20_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-38613-8_8","volume-title":"Integrated Formal Methods","author":"J.-V. Millo","year":"2013","unstructured":"Millo, J.-V., Ramesh, S., Krishna, S.N., Narwane, G.K.: Compositional Verification of Software Product Lines. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 109\u2013123. Springer, Heidelberg (2013)"},{"key":"20_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-642-24690-6_22","volume-title":"Software Engineering and Formal Methods","author":"R. Muschevici","year":"2011","unstructured":"Muschevici, R., Proen\u00e7a, J., Clarke, D.: Modular Modelling of Software Product Lines with Feature Nets. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 318\u2013333. Springer, Heidelberg (2011)"},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer (2005)","DOI":"10.1007\/3-540-28901-1"},{"issue":"1","key":"20_CR56","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.jal.2011.11.002","volume":"10","author":"R. Pugliese","year":"2012","unstructured":"Pugliese, R., Tiezzi, F.: A Calculus for Orchestration of Web Services. Journal of Applied Logic\u00a010(1), 2\u201331 (2012)","journal-title":"Journal of Applied Logic"},{"key":"20_CR57","series-title":"Lecture Notes in Computer Science","volume-title":"Rigorous Software Engineering for Service-Oriented Systems","year":"2011","unstructured":"Wirsing, M., H\u00f6lzl, M. (eds.): SENSORIA. LNCS, vol.\u00a06582. Springer, Heidelberg (2011)"},{"key":"20_CR58","doi-asserted-by":"crossref","unstructured":"Ziadi, T., J\u00e9z\u00e9quel, J.-M.: Software Product Line Engineering with the UML: Deriving Products. In: Software Product Lines: Research Issues in Engineering and Management, pp. 557\u2013588. Springer (2006)","DOI":"10.1007\/978-3-540-33253-4_15"}],"container-title":["Lecture Notes in Computer Science","Software, Services, and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15545-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T18:42:47Z","timestamp":1747766567000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-15545-6_20"}},"subtitle":["From Kandinsky to KandISTI"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319155449","9783319155456"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15545-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}