{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:55:14Z","timestamp":1762458914774,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214608"},{"type":"electronic","value":"9783642214615"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21461-5_3","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T09:25:36Z","timestamp":1307697936000},"page":"44-58","source":"Crossref","is-referenced-by-count":17,"title":["A Model-Checking Tool for Families of Services"],"prefix":"10.1007","author":[{"given":"Patrizia","family":"Asirelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maurice H.","family":"ter Beek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3-4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/s00165-009-0112-0","volume":"22","author":"W.M.P. Aalst van der","year":"2010","unstructured":"van der Aalst, W.M.P., Dumas, M., Gottschalk, F., ter Hofstede, A.H.M., La Rosa, M., Mendling, J.: Preserving correctness during business process model configuration. Formal Asp. Comput.\u00a022(3-4), 459\u2013482 (2010)","journal-title":"Formal Asp. Comput."},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-94-010-0387-2_3","volume-title":"Handbook of Philosophical Logic","author":"L. \u00c5qvist","year":"2002","unstructured":"\u00c5qvist, L.: Deontic Logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol.\u00a08, pp. 147\u2013264. Kluwer, Dordrecht (2002)","edition":"2"},{"key":"3_CR3","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.\u00a06396, pp. 43\u201358. Springer, Heidelberg (2010)"},{"key":"3_CR4","unstructured":"Bertolino, A., Fantechi, A., Gnesi, S., Lami, G., Maccari, A.: Use Case Description of Requirements for Product Lines. In: [16], pp. 12\u201318 (2002)"},{"issue":"2","key":"3_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst.\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT, Cambridge (1999)"},{"key":"3_CR7","first-page":"335","volume-title":"Proceedings 32nd International Conference on Software Engineering (ICSE 2010)","author":"A. Classen","year":"2010","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 32nd International Conference on Software Engineering (ICSE 2010), pp. 335\u2013344. ACM Press, New York (2010)"},{"key":"3_CR8","volume-title":"To appear in: Proceedings 33rd International Conference on Software Engineering (ICSE 2011)","author":"A. Classen","year":"2011","unstructured":"Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic Model Checking of Software Product Lines. To appear in: Proceedings 33rd International Conference on Software Engineering (ICSE 2011). ACM Press, New York (2011)"},{"key":"3_CR9","volume-title":"Software Product Lines: Practices and Patterns","author":"P.C. Clements","year":"2002","unstructured":"Clements, P.C., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley, Reading (2002)"},{"key":"3_CR10","unstructured":"Cohen, S.G., Krut, R.W. (eds.): Proceedings 1st Workshop on Service-Oriented Architectures and Software Product Lines: What is the Connection? (SOAPL 2007). Technical Report CMU\/SEI-2008-SR-006, Carnegie Mellon University (2008)"},{"issue":"2","key":"3_CR11","first-page":"458","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three Logics for Branching Bisimulation. J.\u00a0ACM\u00a042(2), 458\u2013487 (1995)","journal-title":"J.\u00a0ACM"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Fantechi, A., Gnesi, S.: Formal Modelling for Product Families Engineering. In: [15], pp. 193\u2013202 (2008)","DOI":"10.1109\/SPLC.2008.45"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Fantechi, A., Lapadula, A., Pugliese, R., Tiezzi, F., Gnesi, S., Mazzanti, F.: A Logical Verification Methodology for Service-Oriented Computing. To appear in ACM Trans.\u00a0Softw.\u00a0Eng.\u00a0Methodol. (2011)","DOI":"10.1145\/2211616.2211619"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1147249.1147254","volume-title":"Proceedings ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA 2006)","author":"D. Fischbein","year":"2006","unstructured":"Fischbein, D., Uchitel, S., Braberman, V.A.: A Foundation for Behavioural Conformance in Software Product Line Architectures. In: Hierons, R.M., Muccini, H. (eds.) Proceedings ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA 2006), pp. 39\u201348. ACM Press, New York (2006)"},{"volume-title":"Proceedings 12th Software Product Lines Conference (SPLC 2008)","year":"2008","key":"3_CR15","unstructured":"Geppert, B., Pohl, K. (eds.): Proceedings 12th Software Product Lines Conference (SPLC 2008). IEEE Press, Los Alamitos (2008)"},{"key":"3_CR16","unstructured":"Geppert, B., Schmid, K. (eds.): Proceedings International Workshop on Requirements Engineering for Product Lines (REPL 2002). Technical Report ALR-2002-033, Avaya Labs Research (2002)"},{"key":"3_CR17","first-page":"1040","volume-title":"Proceedings International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA 1999)","author":"S. Gnesi","year":"2009","unstructured":"Gnesi, S., Mazzanti, F.: On the Fly Verification of Networks of Automata. In: Arabnia, H.R., et al. (eds.) Proceedings International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA 1999), pp. 1040\u20131046. CSREA Press, Athens (2009)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"3_CR19","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":"3_CR20","doi-asserted-by":"crossref","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.D.: Calculating and Modelling Common Parts of Software Product Lines. In: [15], pp. 203\u2013212 (2008)","DOI":"10.1109\/SPLC.2008.22"},{"issue":"1","key":"3_CR21","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/s10270-003-0019-9","volume":"2","author":"G. Halmans","year":"2003","unstructured":"Halmans, G., Pohl, K.: Communicating the Variability of a Software-Product Family to Customers. Software and System Modeling\u00a02(1), 15\u201336 (2003)","journal-title":"Software and System Modeling"},{"key":"3_CR22","unstructured":"John, I., Muthig, D.: Tailoring Use Cases for Product Line Modeling. In: [16], pp. 26\u201332 (2002)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Krut, R.W., Cohen, S.G. (eds.): Proceedings 2nd Workshop on Service-Oriented Architectures and Software Product Lines: Putting Both Together (SOAPL 2008). In: Thiel, S., Pohl, K. (eds.) Workshop Proceedings 12th Software Product Lines Conference (SPLC 2008), Lero Centre, University of Limerick, pp. 115\u2013147 (2008)","DOI":"10.1109\/SPLC.2008.71"},{"key":"3_CR24","unstructured":"Krut, R.W., Cohen, S.G. (eds.): Proceedings 3rd Workshop on Service-Oriented Architectures and Software Product Lines: Enhancing Variation (SOAPL 2009). In: Muthig, D., McGregor, J.D. (eds.) Proceedings 13th Software Product Lines Conference (SPLC 2009), pp.\u00a0301\u2013302. ACM Press, New York (2009)"},{"key":"3_CR25","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":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 232\u2013246. Springer, Heidelberg (1990)"},{"issue":"2\u20133","key":"3_CR26","first-page":"265","volume":"72","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G.: Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion. Theor.\u00a0Comput.\u00a0Sci.\u00a072(2\u20133), 265\u2013288 (1990)","journal-title":"Theor.\u00a0Comput.\u00a0Sci."},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-71316-6_6","volume-title":"Programming Languages and Systems","author":"K.G. Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: Modal I\/O Automata for Interface and Product Line Theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 64\u201379. Springer, Heidelberg (2007)"},{"key":"3_CR28","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1109\/LICS.1988.5119","volume-title":"Proceedings 3rd Annual Symposium on Logic in Computer Science (LICS 1988)","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Proceedings 3rd Annual Symposium on Logic in Computer Science (LICS 1988), pp. 203\u2013210. IEEE Press, Los Alamitos (1988)"},{"key":"3_CR29","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1109\/ASE.2009.16","volume-title":"Proceedings 24th International Conference on Automated Software Engineering (ASE 2009)","author":"K. Lauenroth","year":"2009","unstructured":"Lauenroth, K., Pohl, K., T\u00f6hning, S.: Model Checking of Domain Artifacts in Product Line Engineering. In: Proceedings 24th International Conference on Automated Software Engineering (ASE 2009), pp. 269\u2013280. IEEE Press, Los Alamitos (2009)"},{"key":"3_CR30","unstructured":"von der Ma\u00dfen, T., Lichter, H.: Modeling Variability by UML Use Case Diagrams. In: [16], pp. 19\u201325 (2002)"},{"key":"3_CR31","unstructured":"Mazzanti, F.: FMC\u00a0v5.0b (2011), \n                  \n                    http:\/\/fmt.isti.cnr.it\/fmc"},{"key":"3_CR32","unstructured":"Muschevici, R., Clarke, D., Proenca, J.: Feature Petri Nets. In: Schaefer, I., Carbon, R. (eds.) Proceedings 1st International Workshop on Formal Methods in Software Product Line Engineering (FMSPLE 2010). University of Lancaster (2010)"},{"key":"3_CR33","volume-title":"The Power of Product Platforms: Building Value and Cost Leadership","author":"M.H. Meyer","year":"1997","unstructured":"Meyer, M.H., Lehnerd, A.P.: The Power of Product Platforms: Building Value and Cost Leadership. The Free Press, New York (1997)"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/3-540-48294-6_22","volume-title":"Static Analysis","author":"M. M\u00fcller-Olm","year":"1999","unstructured":"M\u00fcller-Olm, M., Schmidt, D.A., Steffen, B.: Model-Checking: A Tutorial Introduction. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 330\u2013354. Springer, Heidelberg (1999)"},{"issue":"11","key":"3_CR35","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/MC.2007.400","volume":"40","author":"M. Papazoglou","year":"2007","unstructured":"Papazoglou, M., Traverso, P., Dustdar, S., Leymann, F.: Service-oriented computing: State of the art and research challenges. IEEE Comput.\u00a040(11), 38\u201345 (2007)","journal-title":"IEEE Comput."},{"key":"3_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","volume-title":"Software Product Line Engineering: Foundations, Principles, and Techniques","author":"K. Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, Berlin (2005)"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Razavian, M., Khosravi, R.: Modeling Variability in Business Process Models Using UML. In: Proceedings 5th International Conference on Information Technology: New Generations (ITNG 2008), pp.\u00a082\u201387. IEEE Press, Los Alamitos (2008)","DOI":"10.1109\/ITNG.2008.132"},{"issue":"1","key":"3_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.is.2005.05.003","volume":"32","author":"M. Rosemann","year":"2007","unstructured":"Rosemann, M., van der Aalst, W.M.P.: A configurable reference modelling language. Inf.\u00a0Syst.\u00a032(1), 1\u201323 (2007)","journal-title":"Inf.\u00a0Syst."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21461-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:07:52Z","timestamp":1558296472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21461-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214608","9783642214615"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21461-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}