{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:10:54Z","timestamp":1776373854905,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642336652","type":"print"},{"value":"9783642336669","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33666-9_27","type":"book-chapter","created":{"date-parts":[[2012,9,18]],"date-time":"2012-09-18T16:50:20Z","timestamp":1347987020000},"page":"415-431","source":"Crossref","is-referenced-by-count":69,"title":["From UML and OCL to Relational Logic and Back"],"prefix":"10.1007","author":[{"given":"Mirco","family":"Kuhlmann","sequence":"first","affiliation":[]},{"given":"Martin","family":"Gogolla","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"27_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K. Anastasakis","year":"2010","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Software and System Modeling\u00a09(1), 69\u201386 (2010)","journal-title":"Software and System Modeling"},{"key":"27_CR2","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"J.C. Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"issue":"1-2","key":"27_CR4","first-page":"55","volume":"6","author":"B.F.B. Braga","year":"2010","unstructured":"Braga, B.F.B., Almeida, J.P.A., Guizzardi, G., Benevides, A.B.: Transforming OntoUML into Alloy: towards conceptual model validation using a lightweight formal method. ISSE\u00a06(1-2), 55\u201363 (2010)","journal-title":"ISSE"},{"key":"27_CR5","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":"A.D. 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.\u00a04961, pp. 97\u2013100. Springer, Heidelberg (2008)"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Cabot, J., Clariso, R., Riera, D.: Verification of UML\/OCL Class Diagrams using Constraint Programming. In: IEEE International Conference on Software Testing Verification and Validation Workshop, ICSTW 2008, pp. 73\u201380 (April 2008)","DOI":"10.1109\/ICSTW.2008.54"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/11784180_28","volume-title":"Algebraic Methodology and Software Technology","author":"M. Clavel","year":"2006","unstructured":"Clavel, M., Egea, M.: ITP\/OCL: A Rewriting-Based Validation Tool for UML+OCL Static Class Diagrams. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 368\u2013373. Springer, Heidelberg (2006)"},{"key":"27_CR8","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.G. Garis","year":"2011","unstructured":"Garis, A.G., 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.\u00a07041, pp. 221\u2013236. Springer, Heidelberg (2011)"},{"issue":"1-3","key":"27_CR9","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.\u00a069(1-3), 27\u201334 (2007)","journal-title":"Sci. Comput. Program."},{"key":"27_CR10","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006)"},{"key":"27_CR11","unstructured":"Krieger, M.P., Brucker, A.D.: Extending OCL Operation Contracts with Objective Functions. ECEASST\u00a044 (2011)"},{"key":"27_CR12","unstructured":"Krieger, M.P., Knapp, A.: Executing Underspecified OCL Operation Contracts with a SAT Solver. ECEASST\u00a015 (2008)"},{"key":"27_CR13","unstructured":"Kuhlmann, M., Gogolla, M.: Intrinsic Relational Approach: Transformation of OCL Operations, \n                    \n                      http:\/\/www.db.informatik.uni-bremen.de\/publications\/intern\/IntrinsicApproachOCL2012.pdf"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-31491-9_5","volume-title":"Modelling Foundations and Applications","author":"M. Kuhlmann","year":"2012","unstructured":"Kuhlmann, M., Gogolla, M.: Strengthening SAT-Based Validation of UML\/OCL Models by Representing Collections as Relations. In: Tolvanen, J.P., Vallecillo, A. (eds.) ECMFA 2012. LNCS, vol.\u00a07349, pp. 32\u201348. Springer, Heidelberg (2012)"},{"key":"27_CR15","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.\u00a06705, pp. 290\u2013306. Springer, Heidelberg (2011)"},{"issue":"2","key":"27_CR16","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s10270-010-0174-8","volume":"11","author":"M. Kuhlmann","year":"2012","unstructured":"Kuhlmann, M., Hamann, L., Gogolla, M., B\u00fcttner, F.: A benchmark for OCL engine accuracy, determinateness, and efficiency. Software and System Modeling\u00a011(2), 165\u2013182 (2012)","journal-title":"Software and System Modeling"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Kuhlmann, M., Sohr, K., Gogolla, M.: Comprehensive Two-Level Analysis of Static and Dynamic RBAC Constraints with UML and OCL. In: Baik, J., Massacci, F., Zulkernine, M. (eds.) SSIRI 2011, pp. 108\u2013117. IEEE (2011)","DOI":"10.1109\/SSIRI.2011.18"},{"key":"27_CR18","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.\u00a06981, pp. 592\u2013607. Springer, Heidelberg (2011)"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-24485-8_12","volume-title":"Model Driven Engineering Languages and Systems","author":"S. Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: Semantically Configurable Consistency Analysis for Class and Object Diagrams. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol.\u00a06981, pp. 153\u2013167. Springer, Heidelberg (2011)"},{"key":"27_CR20","unstructured":"Oliv\u00e9, A.: Conceptual Modeling of Information Systems. Springer (2007)"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-642-04238-6_42","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M. Ornaghi","year":"2009","unstructured":"Ornaghi, M., Fiorentini, C., Momigliano, A., Pagano, F.: Applying ASP to UML Model Validation. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol.\u00a05753, pp. 457\u2013463. Springer, Heidelberg (2009)"},{"key":"27_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11901181_37","volume-title":"Conceptual Modeling - ER 2006","author":"A. Queralt","year":"2006","unstructured":"Queralt, A., Teniente, E.: Reasoning on UML Class Diagrams with OCL Constraints. In: Embley, D.W., Oliv\u00e9, A., Ram, S. (eds.) ER 2006. LNCS, vol.\u00a04215, pp. 497\u2013512. Springer, Heidelberg (2006)"},{"key":"27_CR23","unstructured":"Rold\u00e1n, M., Dur\u00e1n, F.: Dynamic Validation of OCL Constraints with mOdCL. ECEASST\u00a044 (2011)"},{"key":"27_CR24","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. The Pearson Higher Education (2004)"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-642-14107-2_26","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"H. Samimi","year":"2010","unstructured":"Samimi, H., Aung, E.D., Millstein, T.D.: Falling Back on Executable Specifications. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 552\u2013576. Springer, Heidelberg (2010)"},{"key":"27_CR26","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. IEEE (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-21470-7_6","volume-title":"Modelling Foundations and Applications","author":"R.V.D. Straeten","year":"2011","unstructured":"Straeten, R.V.D., Puissant, J.P., Mens, T.: Assessing the Kodkod Model Finder for Resolving Model Inconsistencies. In: France, R.B., K\u00fcster, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol.\u00a06698, pp. 69\u201384. Springer, Heidelberg (2011)"},{"key":"27_CR28","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.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"Torlak, E., Vaziri, M., Dolby, J.: MemSAT: checking axiomatic specifications of memory models. In: Zorn, B.G., Aiken, A. (eds.) PLDI, pp. 341\u2013350. ACM (2010)","DOI":"10.1145\/1809028.1806635"},{"key":"27_CR30","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. The Addison-Wesley Object Technology Series. Addison-Wesley (2003)"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33666-9_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:18:12Z","timestamp":1620130692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33666-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642336652","9783642336669"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33666-9_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}