{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:28:43Z","timestamp":1772044123146,"version":"3.50.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,6,13]],"date-time":"2013-06-13T00:00:00Z","timestamp":1371081600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-013-0353-5","type":"journal-article","created":{"date-parts":[[2013,6,12]],"date-time":"2013-06-12T08:51:48Z","timestamp":1371027108000},"page":"5-25","source":"Crossref","is-referenced-by-count":41,"title":["Translating between Alloy specifications and UML class diagrams annotated with OCL"],"prefix":"10.1007","volume":"14","author":[{"given":"Alcino","family":"Cunha","sequence":"first","affiliation":[]},{"given":"Ana","family":"Garis","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Riesco","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,6,13]]},"reference":[{"key":"353_CR1","unstructured":"Anastasakis, K.: A model driven approach for the automated analysis of UML class diagrams. Ph.D. thesis, University of Birmingham, Birmingham (2009)"},{"issue":"1","key":"353_CR2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K Anastasakis","year":"2008","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Softw. Syst. Model. 9(1), 69\u201386 (2008)","journal-title":"Softw. Syst. Model."},{"key":"353_CR3","unstructured":"Bordbar, B., Anastasakis, K.: UML2Alloy: a tool for lightweight modelling of discrete event systems. In: Proceedings of the IADIS International Conference in Applied Computing, pp. 209\u2013216. IADIS Press, Perth (2005)"},{"issue":"1\u20132","key":"353_CR4","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/s11334-009-0120-5","volume":"6","author":"BFB 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. Innov. Syst. Softw. Eng. 6(1\u20132), 55\u201363 (2010)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"353_CR5","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Wolff, B.: HOL-OCL: a formal proof environment for UML\/OCL. In: Proceedings of the 11th International Conference on Fundamental Approaches to Software Engineering, LNCS, vol. 4961, pp. 97\u2013100. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78743-3_8"},{"key":"353_CR6","unstructured":"Cunha, A.: Bounded model checking of temporal formulas with Alloy. Tech. Rep. abs\/1207.2746, CoRR (2012)"},{"key":"353_CR7","doi-asserted-by":"crossref","unstructured":"Demuth, B., Hussmann, H., Loecher, S.: OCL as a specification language for business rules in database applications. In: Proceedings of the 4th International Conference on The Unified Modeling Language, Modeling Languages, Concepts, and Tools, LNCS, vol. 2185, pp. 104\u2013117. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45441-1_9"},{"key":"353_CR8","unstructured":"DresdenOCL website. http:\/\/www.dresden-ocl.org\/index.php\/DresdenOCL"},{"key":"353_CR9","doi-asserted-by":"crossref","unstructured":"Edwards, J., Jackson, D., Torlak, E.: A type system for object models. In: Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 189\u2013199. ACM, New York (2004)","DOI":"10.1145\/1029894.1029921"},{"key":"353_CR10","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading Alloy with actions. In: Proceedings of the 27th International Conference on Software Engineering, pp. 442\u2013451. ACM, New York (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"353_CR11","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Pombo, C.L., Galeotti, J.P., Aguirre, N.: Efficient analysis of DynAlloy specifications. ACM Trans. Softw. Eng. Methodol. 17(1), 4:1\u20134:34 (2007)","DOI":"10.1145\/1314493.1314497"},{"key":"353_CR12","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Frias, M.F.: DynAlloy as a formal method for the analysis of Java programs. In: Software Engineering Techniques: design for quality, IFIP, vol. 227, pp. 249\u2013260. Springer, Berlin (2006)","DOI":"10.1007\/978-0-387-39388-9_24"},{"key":"353_CR13","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., L\u00f3pez Pombo, C.G., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, pp. 25\u201336. ACM, New York (2010)","DOI":"10.1145\/1831708.1831712"},{"key":"353_CR14","doi-asserted-by":"crossref","unstructured":"Garis, A.G., Cunha, A., Riesco, D.: Translating Alloy specifications to UML class diagrams annotated with OCL. In: Proceedings of the 9th International Conference on Software Engineering and Formal Methods, LNCS, vol. 7041, pp. 221\u2013236. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24690-6_16"},{"key":"353_CR15","doi-asserted-by":"crossref","unstructured":"Garis, A.G., Paiva, A.C.R., Cunha, A., Riesco, D.: Specifying UML protocol state machines in Alloy. In: Proceedings of the 9th International Conference on Integrated Formal Methods, LNCS, vol. 7321, pp. 312\u2013326. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-30729-4_22"},{"issue":"3","key":"353_CR16","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1109\/TSE.2010.36","volume":"36","author":"G Georg","year":"2010","unstructured":"Georg, G., Anastasakis, K., Bordbar, B., Houmb, S.H., Toahchoodee, I.R.M.: Verification and trade-off analysis of security properties in UML system models. IEEE Trans. Softw. Eng. 36(3), 338\u2013356 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"353_CR17","doi-asserted-by":"crossref","unstructured":"Ghazi, A.A.E., Taghdiri, M.: Relational reasoning via SMT solving. In: Proceedings of the 17th International Symposium on Formal Methods, LNCS, vol. 6664, pp. 133\u2013148. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-21437-0_12"},{"key":"353_CR18","unstructured":"Gheyi, R., Massoni, T., Borba, P.: Formally introducing Alloy idioms. In: Proceedings of the Brazilian Symposium on Formal, Methods, pp. 22\u201337 (2007)"},{"key":"353_CR19","doi-asserted-by":"crossref","unstructured":"Giannakopoulos, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Towards an operational semantics for Alloy. In: Proceedings of the 16th International Symposium on Formal Methods, LNCS, vol. 5850, pp. 483\u2013498. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-05089-3_31"},{"issue":"4","key":"353_CR20","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1007\/s10270-005-0089-y","volume":"4","author":"M Gogolla","year":"2005","unstructured":"Gogolla, M., Bohling, J., Richters, M.: Validating UML and OCL models in USE by automatic snapshot generation. Softw. Syst. Model. 4(4), 386\u2013398 (2005)","journal-title":"Softw. Syst. Model."},{"key":"353_CR21","doi-asserted-by":"crossref","unstructured":"Hamie, A.: Translating the Object Constraint Language into the Java Modelling Language. In: Proceedings of the 19th ACM Symposium on Applied Computing, pp. 1531\u20131535. ACM, New York (2004)","DOI":"10.1145\/967900.968206"},{"key":"353_CR22","volume-title":"Software Abstractions: Logic, Language, and Analysis, revised edn","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis, revised edn. MIT Press, Cambridge (2012)"},{"key":"353_CR23","doi-asserted-by":"crossref","unstructured":"Kim, J.S., Garlan, D.: Analyzing architectural styles with Alloy. In: Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, pp. 70\u201380. ACM, New York (2006)","DOI":"10.1145\/1147249.1147259"},{"key":"353_CR24","doi-asserted-by":"crossref","unstructured":"Macedo, N., Cunha, A.: Implementing QVT-R bidirectional model transformations using Alloy. In: Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering, LNCS, vol. 7793, pp. 297\u2013311. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-37057-1_22"},{"key":"353_CR25","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J., Rumpe, B.: CD2Alloy: Class diagrams analysis using Alloy revisited. In: Proceedings of the 14th International Conference on Model Driven Engineering Languages and Systems, LNCS, vol. 6981, pp. 592\u2013607. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24485-8_44"},{"key":"353_CR26","doi-asserted-by":"crossref","unstructured":"Massoni, T., Gheyi, R., Borba, P.: Formal refactoring for UML class diagrams. In: Proceedings of the 19th Brazilian Symposium on Software Engineering, pp. 152\u2013167 (2005)","DOI":"10.5753\/sbes.2005.23817"},{"key":"353_CR27","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Jackson, D.: Preventing arithmetic overflows in Alloy. In: Proceedings of the 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, LNCS, vol. 7316, pp. 108\u2013121. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-30885-7_8"},{"key":"353_CR28","doi-asserted-by":"crossref","unstructured":"Mostefaoui, F., Vachon, J.: Verification of Aspect-UML models using Alloy. In: Proceedings of the 10th International Workshop on Aspect-Oriented Modeling, pp. 41\u201348. ACM, New York (2007)","DOI":"10.1145\/1229375.1229382"},{"key":"353_CR29","doi-asserted-by":"crossref","unstructured":"Near, J.P., Jackson, D.: An imperative extension to Alloy. In: Proceedings of the 2nd International Conference on Abstract State Machines, Alloy, B and Z, LNCS, vol. 5977, pp. 118\u2013131. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11811-1_10"},{"key":"353_CR30","unstructured":"OMG: MDA Guide, version 1.0.1 (2003)"},{"key":"353_CR31","unstructured":"OMG: Query\/View\/Transformation, version 1.1 (2011)"},{"key":"353_CR32","unstructured":"OMG: UML Superstructure, version 2.4.1 (2011)"},{"key":"353_CR33","unstructured":"OMG: Object Constraint Language, version 2.3.1 (2012)"},{"key":"353_CR34","doi-asserted-by":"crossref","unstructured":"Shah, S.M.A., Anastasakis, K., Bordbar, B.: From UML to Alloy and back again. In: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation. ACM, New York (2009)","DOI":"10.1145\/1656485.1656489"},{"key":"353_CR35","doi-asserted-by":"crossref","unstructured":"Vakili, A., Day, N.: Temporal logic model checking in Alloy. In: Proceedings of the 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, LNCS, vol. 7316, pp. 150\u2013163. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-30885-7_11"},{"key":"353_CR36","unstructured":"Vaziri, M., Jackson, D.: Some shortcomings of OCL, the Object Constraint Language of UML. In: Proceedings of the 34th International Conference on Technology of Object-Oriented Languages and Systems, pp. 555\u2013562. IEEE (2000)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0353-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0353-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0353-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,2]],"date-time":"2023-07-02T10:19:24Z","timestamp":1688293164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0353-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,13]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["353"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0353-5","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,13]]}}}