{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:21:05Z","timestamp":1743117665871,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319614816"},{"type":"electronic","value":"9783319614823"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-61482-3_11","type":"book-chapter","created":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T07:38:38Z","timestamp":1497857918000},"page":"179-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Finding Achievable Features and Constraint Conflicts for Inconsistent Metamodels"],"prefix":"10.1007","author":[{"given":"Hao","family":"Wu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,6,20]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11663430_14","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"F Jouault","year":"2006","unstructured":"Jouault, F., Kurtev, I.: Transforming models with ATL. In: Bruel, J.-M. (ed.) MODELS 2005. LNCS, vol. 3844, pp. 128\u2013138. Springer, Heidelberg (2006). doi:\n                      10.1007\/11663430_14"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-12107-4_23","volume-title":"Software Language Engineering","author":"S Zschaler","year":"2010","unstructured":"Zschaler, S., Kolovos, D.S., Drivalos, N., Paige, R.F., Rashid, A.: Domain-specific metamodelling languages for software language engineering. In: Brand, M., Ga\u0161evi\u0107, D., Gray, J. (eds.) SLE 2009. LNCS, vol. 5969, pp. 334\u2013353. Springer, Heidelberg (2010). doi:\n                      10.1007\/978-3-642-12107-4_23"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-45594-9_3","volume-title":"Business Process Management","author":"J Becker","year":"2000","unstructured":"Becker, J., Rosemann, M., Uthmann, C.: Guidelines of business process modeling. In: Aalst, W., Desel, J., Oberweis, A. (eds.) Business Process Management. LNCS, vol. 1806, pp. 30\u201349. Springer, Heidelberg (2000). doi:\n                      10.1007\/3-540-45594-9_3"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-21952-8_21","volume-title":"Objects, Models, Components, Patterns","author":"M Kuhlmann","year":"2011","unstructured":"Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 290\u2013306. Springer, Heidelberg (2011). doi:\n                      10.1007\/978-3-642-21952-8_21"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Wille, R., Soeken, M., Drechsler, R.: Debugging of inconsistent UML\/OCL models. In: 2012 DATE, pp. 1078\u20131083 (2012)","DOI":"10.1109\/DATE.2012.6176655"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Wu, H., Monahan, R., Power, J.F.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: 7th TASE, Birmingham, UK (2013)","DOI":"10.1109\/TASE.2013.31"},{"issue":"1","key":"11_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reason."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2018off-the-shelf\u2019 SMT solvers. In: 15th MoDELS, pp. 432\u2013448 (2012)","DOI":"10.1007\/978-3-642-33666-9_28"},{"key":"11_CR9","unstructured":"Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. Electronic Communication of the European Association of Software Science and Technology, vol. 24 (2009)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:\n                      10.1007\/978-3-540-78800-3_24"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations, pp. 85\u2013103 (1972)","DOI":"10.1007\/978-1-4684-2001-2_9"},{"issue":"1\u20133","key":"11_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.scico.2007.01.013","volume":"69","author":"M Gogolla","year":"2007","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1\u20133), 27\u201334 (2007)","journal-title":"Sci. Comput. Program."},{"key":"11_CR13","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK. Elsevier Science (2010)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-38916-0_7","volume-title":"Tests and Proofs","author":"M Gogolla","year":"2013","unstructured":"Gogolla, M., B\u00fcttner, F., Cabot, J.: Initiating a benchmark for UML and OCL analysis tools. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 115\u2013132. Springer, Heidelberg (2013). doi:\n                      10.1007\/978-3-642-38916-0_7"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-21768-5_12","volume-title":"Tests and Proofs","author":"M Soeken","year":"2011","unstructured":"Soeken, M., Wille, R., Drechsler, R.: Encoding OCL data types for SAT-based verification of UML\/OCL models. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 152\u2013170. Springer, Heidelberg (2011). doi:\n                      10.1007\/978-3-642-21768-5_12"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2014.03.023","volume":"93","author":"J Cabot","year":"2014","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: On the verification of UML\/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1\u201323 (2014)","journal-title":"J. Syst. Softw."},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/2491509.2491518","volume":"22","author":"M Balaban","year":"2013","unstructured":"Balaban, M., Maraee, A.: Finite satisfiability of UML class diagrams with constrained class hierarchy. ACM Trans. Softw. Eng. Methodol. 22(3), 24:1\u201324:42 (2013)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Wu, H.: Generating metamodel instances satisfying coverage criteria via SMT solving. In: The 4th MODELSWARD, pp. 40\u201351 (2016)","DOI":"10.5220\/0005650000400051"},{"key":"11_CR19","unstructured":"Beckert, B., Keller, U., Schmitt, P.H.: Translating the object constraint language into first-order predicate logic. In: Verify Workshop at FLoC, Copenhagen, Denmark (2002)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-72901-3_2","volume-title":"Model Driven Architecture- Foundations and Applications","author":"A Maraee","year":"2007","unstructured":"Maraee, A., Balaban, M.: Efficient reasoning about finite satisfiability of UML class diagrams with constrained generalization sets. In: Akehurst, D.H., Vogel, R., Paige, R.F. (eds.) ECMDA-FA 2007. LNCS, vol. 4530, pp. 17\u201331. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-72901-3_2"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-78743-3_8","volume-title":"Fundamental Approaches to Software Engineering","author":"AD Brucker","year":"2008","unstructured":"Brucker, A.D., Wolff, B.: HOL-OCL: a formal proof environment for uml\/ocl. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 97\u2013100. Springer, Heidelberg (2008). doi:\n                      10.1007\/978-3-540-78743-3_8"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2004.09.027","volume":"115","author":"M Kyas","year":"2005","unstructured":"Kyas, M., Fecher, H., de Boer, F.S., Jacob, J., Hooman, J., van der Zwaag, M., Arons, T., Kugler, H.: Formalizing UML models and OCL constraints in PVS. Electron. Notes Theor. Comput. Sci. 115, 39\u201347 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL models using boolean satisfiability. In: DATE, pp. 1341\u20131344 (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"11_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.datak.2011.09.004","volume":"73","author":"A Queralt","year":"2012","unstructured":"Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: finite reasoning on UML\/OCL conceptual schemas. Data Knowl. Eng. 73, 1\u201322 (2012)","journal-title":"Data Knowl. Eng."},{"key":"11_CR25","unstructured":"Dania, C., Clavel, M.: OCL2FOL+: Coping with undefinedness. In: OCL@MoDELS (2013)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-662-49665-7_6","volume-title":"Fundamental Approaches to Software Engineering","author":"O Semer\u00e1th","year":"2016","unstructured":"Semer\u00e1th, O., V\u00f6r\u00f6s, A., Varr\u00f3, D.: Iterative and incremental model generation by logic solvers. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 87\u2013103. Springer, Heidelberg (2016). doi:\n                      10.1007\/978-3-662-49665-7_6"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Przigoda, N., Wille, R., Drechsler, R.: Ground setting properties for an efficient translation of OCL in SMT-based model finding. In: 19th MoDELS, pp. 261\u2013271. ACM (2016)","DOI":"10.1145\/2976767.2976780"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Dania, C., Clavel, M.: OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints. In: 19th MoDELS, pp. 65\u201375. ACM (2016)","DOI":"10.1145\/2976767.2976774"},{"key":"11_CR29","unstructured":"Wu, H., Monahan, R., Power, J.F.: Metamodel instance generation: a systematic literature review. CoRR abs\/1211.6322 (2012)"},{"issue":"3","key":"11_CR30","doi-asserted-by":"publisher","first-page":"23","DOI":"10.4018\/IJISMD.2016070102","volume":"7","author":"H Wu","year":"2016","unstructured":"Wu, H.: An SMT-based approach for generating coverage oriented metamodel instances. Int. J. Inf. Syst. Model. Des. 7(3), 23\u201350 (2016)","journal-title":"Int. J. Inf. Syst. Model. Des."},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez P\u00e9rez, C.A., Buettner, F., Claris\u00f3, R., Cabot, J.: EMFtoCSP: a tool for the lightweight verification of EMF models. In: Formal Methods in Software Engineering: Rigorous and Agile Approaches, Zurich, Suisse (2012)","DOI":"10.1109\/FormSERA.2012.6229788"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of UML\/OCL class diagrams using constraint programming. In: IEEE ICST V&V Workshop, Berlin, Germany, pp. 73\u201380. IEEE Computer Society (2008)","DOI":"10.1109\/ICSTW.2008.54"},{"issue":"2","key":"11_CR33","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodologies 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodologies"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-71209-1_49"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: 37th ICSE. IEEE Press (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-68237-0_23","volume-title":"FM 2008: Formal Methods","author":"E Torlak","year":"2008","unstructured":"Torlak, E., Chang, F.S.-H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 326\u2013341. Springer, Heidelberg (2008). doi:\n                      10.1007\/978-3-540-68237-0_23"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-540-75209-7_30","volume-title":"Model Driven Engineering Languages and Systems","author":"K Anastasakis","year":"2007","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436\u2013450. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-75209-7_30"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-24485-8_44","volume-title":"Model Driven Engineering Languages and Systems","author":"S Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: class diagrams analysis using alloy revisited. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 592\u2013607. Springer, Heidelberg (2011). doi:\n                      10.1007\/978-3-642-24485-8_44"},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-24690-6_16","volume-title":"Software Engineering and Formal Methods","author":"A Garis","year":"2011","unstructured":"Garis, A., Cunha, A., Riesco, D.: Translating alloy specifications to UML class diagrams annotated with OCL. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 221\u2013236. Springer, Heidelberg (2011). doi:\n                      10.1007\/978-3-642-24690-6_16"},{"key":"11_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-642-33666-9_27","volume-title":"Model Driven Engineering Languages and Systems","author":"M Kuhlmann","year":"2012","unstructured":"Kuhlmann, M., Gogolla, M.: From UML and OCL to relational logic and back. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 415\u2013431. Springer, Heidelberg (2012). doi:\n                      10.1007\/978-3-642-33666-9_27"}],"container-title":["Lecture Notes in Computer Science","Modelling Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-61482-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:30:56Z","timestamp":1558319456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-61482-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319614816","9783319614823"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-61482-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"20 June 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ECMFA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Conference on Modelling Foundations and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marburg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"19 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ecmdafa2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ecmfaconference.wixsite.com\/ecmfa2017","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}