{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:10:55Z","timestamp":1776373855723,"version":"3.51.2"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319668444","type":"print"},{"value":"9783319668451","type":"electronic"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_23","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"348-356","source":"Crossref","is-referenced-by-count":17,"title":["MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams"],"prefix":"10.1007","author":[{"given":"Hao","family":"Wu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"23_CR1","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: 10.1007\/978-3-642-21952-8_21"},{"key":"23_CR2","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":"23_CR3","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"},{"key":"23_CR4","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":"23_CR5","doi-asserted-by":"crossref","unstructured":"Wu, H.: Finding achievable features and contraint conflicts for inconsistent metamodels. In: 13th ECMFA (2017, to appear)","DOI":"10.1007\/978-3-319-61482-3_11"},{"issue":"1\u20133","key":"23_CR6","doi-asserted-by":"crossref","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."},{"issue":"1","key":"23_CR7","doi-asserted-by":"crossref","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":"23_CR8","unstructured":"Beckert, B., Keller, U., Schmitt, P.H.: Translating the object constraint language into first-order predicate logic. In: FLoC @ 3rd Federated Logic Conferences, Denmark (2002)"},{"key":"23_CR9","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: 10.1007\/978-3-540-72901-3_2"},{"key":"23_CR10","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: 10.1007\/978-3-642-21768-5_12"},{"key":"23_CR11","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":"23_CR12","first-page":"13","volume":"24","author":"M Clavel","year":"2009","unstructured":"Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. ECEASST 24, 13 (2009)","journal-title":"ECEASST"},{"key":"23_CR13","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: 10.1007\/978-3-540-78743-3_8"},{"key":"23_CR14","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: 10.1007\/978-3-540-75209-7_30"},{"key":"23_CR15","volume-title":"Verification of Object-Oriented Software: The KeY Approach","author":"B Beckert","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, Heidelberg (2007)"},{"key":"23_CR16","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":"23_CR17","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: 10.1007\/978-3-540-71209-1_49"},{"key":"23_CR18","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: SEMF: Rigorous and Agile Approaches, Zurich, Suisse (2012)","DOI":"10.1109\/FormSERA.2012.6229788"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of UML\/OCL class diagrams using constraint programming. In: IEEE STV&V Workshop, pp. 73\u201380. IEEE Computer Society, Berlin, Germany (2008)","DOI":"10.1109\/ICSTW.2008.54"},{"key":"23_CR20","doi-asserted-by":"crossref","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."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T16:51:56Z","timestamp":1570035116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}