{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T20:23:58Z","timestamp":1791231838064,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540752080","type":"print"},{"value":"9783540752097","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75209-7_30","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T03:42:37Z","timestamp":1189482157000},"page":"436-450","source":"Crossref","is-referenced-by-count":133,"title":["UML2Alloy: A Challenging Model Transformation"],"prefix":"10.1007","author":[{"given":"Kyriakos","family":"Anastasakis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Behzad","family":"Bordbar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Geri","family":"Georg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Indrakshi","family":"Ray","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"OMG: UML Infrastructure Document: formal\/05-07-05, \n                    \n                      http:\/\/www.omg.org"},{"key":"30_CR2","unstructured":"Marcano, R., Levy, N.: Using B formal specifications for analysis and verification of UML\/OCL models. In: Workshop on consistency problems in UML-based software development. 5th International Conference on the Unified Modeling Language, Dresden, Germany (2002)"},{"key":"30_CR3","unstructured":"Kim, S.K.: A Metamodel-based Approach to Integrate Object-Oriented Graphical and Formal Specification Techniques. PhD thesis, University of Queensland, Brisbane, Australia (2002)"},{"key":"30_CR4","unstructured":"Evans, A., France, R., Grant, E.: Towards Formal Reasoning with UML Models. In: Proceedings of the OOPSLA 1999 Workshop on Behavioral Semantics (1999)"},{"key":"30_CR5","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, London, England (2006)"},{"key":"30_CR6","unstructured":"Jackson, D.: Alloy Analyzer website, \n                    \n                      http:\/\/alloy.mit.edu\/"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/978-3-540-39979-7_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"M. Taghdiri","year":"2003","unstructured":"Taghdiri, M., Jackson, D.: A lightweight formal analysis of a multicast key management scheme. In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol.\u00a02767, pp. 240\u2013256. Springer, Heidelberg (2003)"},{"key":"30_CR8","unstructured":"Georg, G., Bieman, J., France, R.B.: Using Alloy and UML\/OCL to Specify Run-Time Configuration Management: A Case Study. In: Evans, A., France, R., Moreira, A., Rumpe, B. (eds.) Practical UML-Based Rigorous Development Methods - Countering or Integrating the eXtremists. LNI, German Informatics Society, vol. P-7, pp. 128\u2013141 (2001)"},{"key":"30_CR9","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1145\/1007512.1007535","volume-title":"ISSTA 2004","author":"G. Dennis","year":"2004","unstructured":"Dennis, G., Seater, R., Rayside, D., Jackson, D.: Automating commutativity analysis at the design level. In: ISSTA 2004. ACM SIGSOFT international symposium on Software testing and analysis, pp. 165\u2013174. ACM Press, New York (2004)"},{"key":"30_CR10","unstructured":"Richters, M.: A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universitaet Bremen, Logos Verlag, Berlin, BISS Monographs, No. 14 (2002)"},{"key":"30_CR11","first-page":"209","volume-title":"IADIS International Conference in Applied Computing 2005","author":"B. Bordbar","year":"2005","unstructured":"Bordbar, B., Anastasakis, K.: UML2Alloy: A tool for lightweight modelling of Discrete Event Systems. In: Guimar\u00e3es, N., Isa\u00edas, P. (eds.) IADIS International Conference in Applied Computing 2005, vol.\u00a01, pp. 209\u2013216. IADIS Press, Algarve, Portugal (2005)"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/11681885_5","volume-title":"Trends in Enterprise Application Architecture","author":"B. Bordbar","year":"2006","unstructured":"Bordbar, B., Anastasakis, K.: MDA and Analysis of Web Applications. In: Draheim, D., Weber, G. (eds.) TEAA 2005. LNCS, vol.\u00a03888, pp. 44\u201355. Springer, Heidelberg (2006)"},{"key":"30_CR13","series-title":"The Addison-Wesley Object Technology Series","volume-title":"MDA Explained: The Model Driven Architecture-Practice and Promise","author":"A. Kleppe","year":"2003","unstructured":"Kleppe, A., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture-Practice and Promise. The Addison-Wesley Object Technology Series. Addison-Wesley, Reading (2003)"},{"key":"30_CR14","unstructured":"OMG: MOF Core v. 2.0 Document Id: formal\/06-01-01, \n                    \n                      http:\/\/www.omg.org"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/11880240_25","volume-title":"Model Driven Engineering Languages and Systems","author":"D.H. Akehurst","year":"2006","unstructured":"Akehurst, D.H., Bordbar, B., Evans, M.J., Howells, W.G.J., McDonald-Maier, K.D.: SiTra: Simple transformations in java. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol.\u00a04199, pp. 351\u2013364. Springer, Heidelberg (2006)"},{"key":"30_CR16","unstructured":"OMG: UML: Superstructure. Document id: formal\/05-07-04, \n                    \n                      http:\/\/www.omg.org"},{"key":"30_CR17","unstructured":"OMG: OCL Version 2.0 Document id: formal\/06-05-01, \n                    \n                      http:\/\/www.omg.org"},{"key":"30_CR18","volume-title":"Compilers: principles, techniques, and tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: principles, techniques, and tools. Addison-Wesley, Reading (1986)"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/11663430_17","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"M. Wimmer","year":"2006","unstructured":"Wimmer, M., Kramler, G.: Bridging grammarware and modelware. In: Bruel, J.M. (ed.) MoDELS 2005. LNCS, vol.\u00a03844, pp. 159\u2013168. Springer, Heidelberg (2006)"},{"key":"30_CR20","unstructured":"TLSWG: SSL 3.0 specification (1996), \n                    \n                      http:\/\/wp.netscape.com\/eng\/ssl3"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Georg, G., Anastasakis, K., Bordbar, B., Houmb, S.H., Ray, I., Toahchoodee, M.: Verification and trade-off analysis of security properties in UML system models. Transaction. In: Software Engineering. Special Issue on Security (submitted)","DOI":"10.1109\/TSE.2010.36"},{"key":"30_CR22","unstructured":"Jackson, D.: A Comparison of Object Modelling Notations: Alloy, UML and Z (August 1999), Available at \n                    \n                      http:\/\/sdg.lcs.mit.edu\/publications.html"},{"key":"30_CR23","unstructured":"Vaziri, M., Jackson, D.: Some Shortcomings of OCL, the Object Constraint Language of UML. In: Technology of Object-Oriented Languages and Systems (TOOLS 34\u201900), Santa Barbara, California, pp. 555\u2013562 (2000)"},{"key":"30_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-540-48480-6_8","volume-title":"The Unified Modeling Language. UML 1998: Beyond the Notation","author":"M. Gogolla","year":"1999","unstructured":"Gogolla, M., Richters, M.: Transformation rules for UML class diagrams. In: B\u00e9zivin, J., Muller, P.-A. (eds.) The Unified Modeling Language. UML 1998: Beyond the Notation. LNCS, vol.\u00a01618, pp. 92\u2013106. Springer, Heidelberg (1999)"},{"issue":"15","key":"30_CR25","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1016\/S0950-5849(03)00131-9","volume":"45","author":"C. Wallace","year":"2003","unstructured":"Wallace, C.: Using Alloy in process modelling. Information and Software Technology\u00a045(15), 1031\u20131043 (2003)","journal-title":"Information and Software Technology"},{"key":"30_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/11880240_14","volume-title":"Model Driven Engineering Languages and Systems","author":"A. Zito","year":"2006","unstructured":"Zito, A., Diskin, Z., Dingel, J.: Package Merge in UML 2: Practice vs. Theory? In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol.\u00a04199, pp. 185\u2013199. Springer, Heidelberg (2006)"},{"key":"30_CR27","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Upper Saddle River, NJ (1996)"},{"key":"30_CR28","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)"},{"key":"30_CR29","unstructured":"He, Y.: Comparison of the modeling languages Alloy and UML. In: Arabnia, H.R., Reza, H. (eds.) SERP 2006. Software Engineering Research and Practice, Las Vegas, Nevada, vol.\u00a02, pp. 671\u2013677 (2006)"},{"issue":"3","key":"30_CR30","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1145\/111197.111212","volume":"16","author":"M. Negri","year":"1991","unstructured":"Negri, M., Pelagatti, G., Sbattella, L.: Formal semantics of SQL queries. ACM Transactions on Database Systems (TODS)\u00a016(3), 513\u2013534 (1991)","journal-title":"ACM Transactions on Database Systems (TODS)"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75209-7_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:56:02Z","timestamp":1619506562000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75209-7_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752080","9783540752097"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75209-7_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}