{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T12:02:21Z","timestamp":1791201741563,"version":"4.2.0"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,12,12]],"date-time":"2008-12-12T00:00:00Z","timestamp":1229040000000},"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":[[2010,1]]},"DOI":"10.1007\/s10270-008-0110-3","type":"journal-article","created":{"date-parts":[[2008,12,11]],"date-time":"2008-12-11T05:02:34Z","timestamp":1228971754000},"page":"69-86","source":"Crossref","is-referenced-by-count":144,"title":["On challenges of model transformation from UML to Alloy"],"prefix":"10.1007","volume":"9","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","published-online":{"date-parts":[[2008,12,12]]},"reference":[{"key":"110_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-book: assigning programs to meanings. Cambridge University Press, New York, 1996. ISBN 0-521- 49619-5","DOI":"10.1017\/CBO9780511624162"},{"key":"110_CR2","unstructured":"Agrawal, A.: Graph rewriting and transformation (GReAT): a solution for the model integrated computing (MIC) Bottleneck. In: 18th IEEE International Conference on Automated Software Engineering (ASE 2003), Montreal, Canada, pp. 364\u2013368. IEEE Computer Society, New York (2003). http:\/\/csdl.computer.org\/comp\/proceedings\/ase\/2003\/2035\/00\/20350364abs.htm ."},{"key":"110_CR3","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)"},{"issue":"1","key":"110_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10270-006-0020-1","volume":"6","author":"D. Akehurst","year":"2007","unstructured":"Akehurst D., Howells G., Mcdonald-Maier K.: Implementing associations: UML 2.0 to Java 5. Softw. Syst. Model. 6(1), 3\u201335 (2007). doi: 10.1007\/s10270-006-0020-1","journal-title":"Softw. Syst. Model."},{"key":"110_CR5","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.) Model Driven Engineering Languages and Systems, 9th International Conference, MoDELS 2006. Lecture Notes in Computer Science, vol. 4199, pp. 351\u2013364, Genova, Italy, 2006. Springer, Heidelberg"},{"key":"110_CR6","unstructured":"Anastasakis, K., Bordbar, B.: Using Alloy for the Analysis of Model Transformations: A Case Study. Technical report, School of Computer Science, The University of Birmingham, UK, 2007. (In Preperation). http:\/\/www.cs.bham.ac.uk\/kxa\/files\/analysis\/techrep07.pdf"},{"key":"110_CR7","doi-asserted-by":"crossref","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.) ACM\/IEEE 10th International Conference on Model Driven Engineering Languages and Systems. LNCS, vol. 4735, pp. 436\u2013450, Nashville, USA. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-75209-7_30"},{"issue":"3","key":"110_CR8","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/S0169-023X(96)00013-4","volume":"20","author":"A. Artale","year":"1996","unstructured":"Artale A., Franconi E., Guarino N., Pazzi L.: Part-whole relations in object-centered systems: An overview. Data Knowl. Eng. 20(3), 347\u2013383 (1996)","journal-title":"Data Knowl. Eng."},{"key":"110_CR9","unstructured":"Babkin, E.: Transformation of ontologies: theoretical foundations and software platform for complex distributed systems. PhD thesis, Computer Science of INSA De Rouen, December 2007"},{"key":"110_CR10","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: Verification of Object-Oriented Software. The KeY Approach. Springer, New York, 2007. ISBN 354068977X","DOI":"10.1007\/978-3-540-69061-0"},{"key":"110_CR11","doi-asserted-by":"crossref","unstructured":"Bordbar, B., Anastasakis, K.: MDA and Analysis of web applications. In: Trends in Enterprise Application Architecture (TEAA) 2005. Lecture notes in Computer Science, vol. 3888, pp. 44\u201355, Trondheim, Norway (2005a)","DOI":"10.1007\/11681885_5"},{"key":"110_CR12","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. 1, pp. 209\u2013216, Algarve, Portugal, February 2005b. IADIS Press. ISBN 972-99353-6-X"},{"key":"110_CR13","doi-asserted-by":"crossref","unstructured":"Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21(10), 785\u2013798. ISSN 0098-5589. doi: 10.1109\/32.469460 (1995)","DOI":"10.1109\/32.469460"},{"key":"110_CR14","unstructured":"Brucker, A.D.: An Interactive Proof Environment for Object-oriented Specifications. PhD thesis, ETH Zurich, March 2007. http:\/\/www.brucker.ch\/bibliography\/abstract\/brucker-interactive-2007 . ETH Dissertation No. 17097"},{"key":"110_CR15","doi-asserted-by":"crossref","unstructured":"Dennis, G., Seater, R., Rayside, D., Jackson, D.: Automating commutativity analysis at the design level. In: ISSTA \u201904: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, pp. 165\u2013174. ACM Press, New York. ISBN 1-58113-820-2. doi: 10.1145\/1007512.1007535 (2004)","DOI":"10.1145\/1007512.1007535"},{"key":"110_CR16","unstructured":"Evans, A., France, R., Grant, E.: Towards Formal Reasoning with UML Models. In: Proceedings of the OOPSLA\u201999 Workshop on Behavioral Semantics (1999)"},{"key":"110_CR17","doi-asserted-by":"crossref","unstructured":"Fleurey, F., Steel, J., Baudry, B.: Validation in model-driven engineering: testing model transformations. In: First International Workshop on Model, Design and Validation, pp. 29\u2013 40, 2004","DOI":"10.1109\/MODEVA.2004.1425846"},{"key":"110_CR18","unstructured":"Fowler, M.: UML Distilled: A Brief Guide to the Standard Object Modeling Language. Object Technology Series, 3rd edn. Addison Wesley, Reading. ISBN 0321193687 (2003)"},{"key":"110_CR19","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\u2014Countering or Integrating the eXtremists., vol P-7 of LNI, pp. 128\u2013141. German Informatics Society (2001)"},{"key":"110_CR20","doi-asserted-by":"crossref","unstructured":"Georg, G., Ray, I., Anastasakis, K., Bordbar, B., Toahchoodee, M., Houmb, S.H.: An Aspect-Oriented Methodology for Desinging Secure Applications. Information and Software Technology. Special Issue on Model Based Development for Secure Information Systems. doi: 10.1016\/j.infsof.2008.05.004 . (accepted)","DOI":"10.1016\/j.infsof.2008.05.004"},{"issue":"4","key":"110_CR21","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. J. Softw. Syst. Model. 4(4), 386\u2013398 (2005)","journal-title":"J. Softw. Syst. Model."},{"key":"110_CR22","doi-asserted-by":"crossref","unstructured":"Gogolla, M., Richters, M.: Transformation rules for UML class diagrams. In: \u201cUML\u201d: \u201998: Selected papers from the First International Workshop on The Unified Modeling Language \u201cUML\u201d: \u201998, pp. 92\u2013106, London, UK. Springer, Heidelberg. ISBN 3-540-66252-9 (1999)","DOI":"10.1007\/978-3-540-48480-6_8"},{"key":"110_CR23","doi-asserted-by":"crossref","unstructured":"Gogolla, M., Richters, M.: Expressing UML class diagrams properties with OCL. In: Object Modeling with the OCL, The Rationale behind the Object Constraint Language, pp. 85\u2013114, London, UK. Springer, Heidelberg. ISBN 3-540-43169-1 (2002)","DOI":"10.1007\/3-540-45669-4_6"},{"key":"110_CR24","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel D., Kozen D., Tiuryn J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"110_CR25","unstructured":"He, Y.: Comparison of the modeling languages Alloy and UML. In: Arabnia, H.R., Reza, H. (eds.) Software Engineering Research and Practice, SERP 2006, vol. 2, pp. 671\u2013677, Las Vegas, Nevada, USA (2006)"},{"key":"110_CR26","doi-asserted-by":"crossref","unstructured":"Henderson-Sellers, B., Barbier, F.: What is this thing called aggregation? In: TOOLS \u201999: Proceedings of the Technology of Object-Oriented Languages and Systems, Washington, DC, USA, p. 236. IEEE Computer Society, New York. ISBN 0-7695-0275-X (1999)","DOI":"10.1109\/TOOLS.1999.779016"},{"key":"110_CR27","unstructured":"Jackson, D.: Alloy Analyzer website. http:\/\/alloy.mit.edu\/"},{"key":"110_CR28","unstructured":"Jackson, D.: A Comparison of Object Modelling Notations: Alloy, UML and Z. Available at: http:\/\/sdg.lcs.mit.edu\/publications.html , August 1999"},{"key":"110_CR29","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 (2006)"},{"key":"110_CR30","doi-asserted-by":"crossref","unstructured":"Jouault, F., Kurtev, I.: Transforming Models with ATL. In: Satellite Events at the MoDELS 2005 Conference. LNCS, vol. 3844, pp. 128\u2013138. Springer, Heidelberg (2006). http:\/\/www.lina.sciences.univ-nantes.fr\/Publications\/2006\/JK06a","DOI":"10.1007\/11663430_14"},{"key":"110_CR31","unstructured":"Kent Modelling Framework. http:\/\/www.cs.kent.ac.uk\/projects\/kmf . School of Computing, University of Kent."},{"key":"110_CR32","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":"110_CR33","unstructured":"Kleppe, A., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture\u2013Practice and Promise. The Addison-Wesley Object Technology Series. Addison-Wesley, Reading. ISBN 032119442X (2003)"},{"key":"110_CR34","doi-asserted-by":"crossref","unstructured":"K\u00fcster, J.M., Abd-El-Razik, M.: Validation of model transformations\u2014first experiences using a white box approach. In: K\u00fchne, T. (ed.) MoDELS Workshops. Lecture Notes in Computer Science, vol. 4364, pp. 193\u2013204. Springer, Heidelberg. ISBN 978-3-540-69488-5 (2006)","DOI":"10.1007\/978-3-540-69489-2_24"},{"key":"110_CR35","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schr\u00f6eder public-key protocol using FDR. In: TACAs \u201996: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pp. 147\u2013166, London, UK. Springer, Heidelberg. ISBN 3-540-61042-1 (1996)","DOI":"10.1007\/3-540-61042-1_43"},{"key":"110_CR36","unstructured":"Marcano, R., Levy, N.: Using B formal specifications for analysis and verification of UML\/OCL models. In: Kuzniarz, L., Reggio, G., Sourrouille, J.L., Huzar, Z. (eds.) Blekinge Institute of Technology, Research Report 2002:06., pp. 91\u2013105. Department of Software Engineering and Computer Science, Blekinge Institute of Technology (2002)"},{"key":"110_CR37","doi-asserted-by":"crossref","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM, 21(12), 993\u2013999. ISSN 0001-0782. doi: 10.1145\/359657.359659 (1978)","DOI":"10.1145\/359657.359659"},{"key":"110_CR38","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283","author":"T. Nipkow","year":"2002","unstructured":"Nipkow T., Paulson L.C., Wenzel M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"110_CR39","doi-asserted-by":"crossref","unstructured":"Olsen, G.K., Oldevik, J.: Scenarios of traceability in model to text transformations. In: Akehurst, D.H., Vogel, R., Paige, R.F. (eds.) ECMDA-FA. Lecture Notes in Computer Science, vol. 4530, pp. 144\u2013156. Springer, Heidelberg. ISBN 978-3-540-72900-6 (2007)","DOI":"10.1007\/978-3-540-72901-3_11"},{"key":"110_CR40","unstructured":"OMG. MOF Core v. 2.0, . Document Id: formal\/06-01-01. http:\/\/www.omg.org"},{"key":"110_CR41","unstructured":"OMG. MOF Models to Text Transformation Language Final Adopted Specification, . Document: ptc\/06-11-01. http:\/\/www.omg.org"},{"key":"110_CR42","unstructured":"OMG. OCL Version 2.0, . Document id: formal\/06-05-01. http:\/\/www.omg.org"},{"key":"110_CR43","unstructured":"OMG. UML Infrastructure, . Document: formal\/05-07-05. http:\/\/www.omg.org"},{"key":"110_CR44","unstructured":"OMG. UML Infrastructure, . Document: formal\/2007-11-04. http:\/\/www.omg.org"},{"key":"110_CR45","unstructured":"OMG. UML: Superstructure. Version 2.0, . Document id: formal\/05-07-04. http:\/\/www.omg.org"},{"key":"110_CR46","unstructured":"OMG. UML: Superstructure. Version 2.1.2, . Document id: formal\/2007-11-02. http:\/\/www.omg.org"},{"key":"110_CR47","unstructured":"Pons, C., Garcia, D.: A lightweight approach for the semantic validation of model refinements. In: MBT 2008. Fourth Workshop on Model-Based Testing., 2008"},{"key":"110_CR48","doi-asserted-by":"crossref","unstructured":"Ramananandro, T.: Mondex, an electronic purse: specification and refinement checks with the alloy model-finding method. Form. Asp. Comput. 20(1):21\u201339. ISSN 0934-5043. doi: 10.1007\/s00165-007-0058-z (2007)","DOI":"10.1007\/s00165-007-0058-z"},{"key":"110_CR49","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":"110_CR50","volume-title":"The Unified Modeling Language Reference Manual. The Addison-Wesley Object Technology Series","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh J., Jacobson I., Booch G.: The Unified Modeling Language Reference Manual. The Addison-Wesley Object Technology Series. Addison-Wesley, Harlow (1999)"},{"key":"110_CR51","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, Montreal, Canada, pp. 94\u2013105. IEEE Computer Society, New York (2003)","DOI":"10.1109\/ASE.2003.1240298"},{"key":"110_CR52","doi-asserted-by":"crossref","unstructured":"Taghdiri, M., Jackson, D.: A lightweight formal analysis of a multicast key management scheme. In: Formal Techniques for Networked and Distributed Systems\u2014FORTE 2003. Lecture Notes in Computer Science, vol. 2767, pp. 240\u2013256. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-39979-7_16"},{"key":"110_CR53","unstructured":"TLSWG. SSL 3.0 specification, 1996. http:\/\/wp.netscape.com\/eng\/ssl3"},{"key":"110_CR54","volume-title":"Knowledge flow analysis for security protocols. Technical Report MIT-CSAIL-TR-2005-066, Computer Science and Artificial Intelligence Laboratory","author":"E. Torlak","year":"2005","unstructured":"Torlak E., van Dijk M., Gassend B., Jackson D., Devadas S.: Knowledge flow analysis for security protocols. Technical Report MIT-CSAIL-TR-2005-066, Computer Science and Artificial Intelligence Laboratory. MIT, Cambridge (2005)"},{"key":"110_CR55","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), pp. 555\u2013562, Santa Barbara, California, USA (2000)"},{"issue":"15","key":"110_CR56","doi-asserted-by":"crossref","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. Inf. Softw. Technol 45(15), 1031\u20131043 (2003)","journal-title":"Inf. Softw. Technol"},{"key":"110_CR57","doi-asserted-by":"crossref","unstructured":"Wimmer, M., Kramler, G.: Bridging grammarware and modelware. In Bruel, J.-M. (ed) MoDELS Satellite Events. Lecture Notes in Computer Science, vol. 3844, pp. 159\u2013168. Springer, Heidelberg. ISBN 3-540-31780-5 (2006)","DOI":"10.1007\/11663430_17"},{"key":"110_CR58","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, USA (1996)"},{"key":"110_CR59","unstructured":"Zito, A., Dingel, J.: Modeling UML 2 package merge with Alloy. In Proceedings of the 1st Alloy Workshop (Alloy \u201906), pp. 86\u201395, Portland, Oregon (2006)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-008-0110-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-008-0110-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-008-0110-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T11:55:26Z","timestamp":1559130926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-008-0110-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,12]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["110"],"URL":"https:\/\/doi.org\/10.1007\/s10270-008-0110-3","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12,12]]}}}