{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T15:02:24Z","timestamp":1760799744467},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642546235"},{"type":"electronic","value":"9783642546242"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-642-54624-2_11","type":"book-chapter","created":{"date-parts":[[2014,2,28]],"date-time":"2014-02-28T22:42:59Z","timestamp":1393627379000},"page":"212-228","source":"Crossref","is-referenced-by-count":3,"title":["Dynamic Validation of Maude Prototypes of UML Models"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[]},{"given":"Manuel","family":"Rold\u00e1n","sequence":"additional","affiliation":[]},{"given":"Antonio","family":"Moreno","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9 Mar\u00eda","family":"\u00c1lvarez","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"UML-B, http:\/\/wiki.event-b.org\/index.php\/UML-B"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Ameedeen, M.A., Bordbar, B.: A model driven approach to represent sequence diagrams as free choice Petri Nets. In: 12th Intl. IEEE Enterprise Distributed Object Computing Conf., ECOC 2008, pp. 213\u2013221. IEEE (2008)","DOI":"10.1109\/EDOC.2008.42"},{"issue":"1","key":"11_CR3","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":"11_CR4","unstructured":"Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide, 2nd edn. Addison-Wesley (2005)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-540-78743-3_28","volume-title":"Fundamental Approaches to Software Engineering","author":"A. Boronat","year":"2008","unstructured":"Boronat, A., Meseguer, J.: An Algebraic Semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 377\u2013391. Springer, Heidelberg (2008)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Boronat, A., Meseguer, J.: Algebraic semantics of ocl-constrained metamodel specifications. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol.\u00a033, pp. 96\u2013115. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02571-6_7"},{"key":"11_CR7","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":"11_CR8","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of uml\/ocl class diagrams using constraint programming. In: First Intl. Conf. on Software Testing, Verification, and Validation, ICST 2008, pp. 73\u201380. IEEE (2008)","DOI":"10.1109\/ICSTW.2008.54"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-30982-3_3","volume-title":"Formal Methods for Model-Driven Engineering","author":"J. Cabot","year":"2012","unstructured":"Cabot, J., Gogolla, M.: Object constraint language (OCL): A definitive guide. In: Bernardo, M., Cortellessa, V., Pierantonio, A. (eds.) SFM 2012. LNCS, vol.\u00a07320, pp. 58\u201390. Springer, Heidelberg (2012)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/11787044_20","volume-title":"Model Driven Architecture \u2013 Foundations and Applications","author":"J. Cabot","year":"2006","unstructured":"Cabot, J., Teniente, E.: Constraint support in MDA tools: A survey. In: Rensink, A., Warmer, J. (eds.) ECMDA-FA 2006. LNCS, vol.\u00a04066, pp. 256\u2013267. Springer, Heidelberg (2006)"},{"issue":"2","key":"11_CR11","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and Programming in Rewriting Logic. Theoretical Computer Science\u00a0285(2), 187\u2013243 (2002)","journal-title":"Theoretical Computer Science"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73859-6_12","volume-title":"Algebra and Coalgebra in Computer Science","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Hendrix, J., Lucas, S., Meseguer, J., \u00d6lveczky, P.: The Maude Formal Tool Environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol.\u00a04624, pp. 173\u2013178. Springer, Heidelberg (2007)"},{"key":"11_CR14","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)"},{"issue":"3","key":"11_CR15","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1147\/sj.453.0621","volume":"45","author":"K. Czarnecki","year":"2006","unstructured":"Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Syst. J.\u00a045(3), 621\u2013645 (2006)","journal-title":"IBM Syst. J."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Gogolla, M., Rold\u00e1n, M.: Tracing Properties of UML and OCL Models with Maude. In: Dur\u00e1n, F., Rusu, V. (eds.) Proc. of Intl. Workshop on Algebraic Methods in Model-Based Software Engineering, AMMSE 2011, Electronic Proceedings in Theoretical Computer Science (2011)","DOI":"10.4204\/EPTCS.56.6"},{"key":"11_CR17","unstructured":"Dur\u00e1n, F., Rold\u00e1n, M.: Validating OCL constraints on Maude prototypes of UML models (2012), http:\/\/maude.lcc.uma.es\/mOdCL\/docs\/mOdCL-validation.pdf"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Fern\u00e1ndez-Alem\u00e1n, J.L., Toval-\u00c1lvarez, A.: Seamless Formalizing the UML Semantics through Metamodels. In: Siau, K., Halpin, T. (eds.) Unified Modeling Language: Systems Analysis, Design and Development Issues, pp. 224\u2013248. Idea Group Publishing (2001)","DOI":"10.4018\/978-1-930708-05-1.ch014"},{"issue":"1-3","key":"11_CR19","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. Science of Computer Programming\u00a069(1-3), 27\u201334 (2007)","journal-title":"Science of Computer Programming"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-33666-9_16","volume-title":"Model Driven Engineering Languages and Systems","author":"L. Hamann","year":"2012","unstructured":"Hamann, L., Hofrichter, O., Gogolla, M.: On integrating structure and behavior modeling with OCL. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol.\u00a07590, pp. 235\u2013251. Springer, Heidelberg (2012)"},{"issue":"1-2","key":"11_CR21","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.08.002","volume":"72","author":"F. Jouault","year":"2008","unstructured":"Jouault, F., Allilaire, F., B\u00e9zivin, J., Kurtev, I.: ATL: A model transformation tool. Science of Computer Programming\u00a072(1-2), 31\u201339 (2008)","journal-title":"Science of Computer Programming"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11663430_14","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"F. Jouault","year":"2006","unstructured":"Jouault, F., Kurtev, I.: Transforming models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol.\u00a03844, pp. 128\u2013138. Springer, Heidelberg (2006)"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Knapp, A.: Generating Rewrite Theories from UML Collaborations. In: Futatsugi, K., Nakagawa, A., Tamai, T. (eds.) CAFE: An Industrial-Strength Algebraic Formal Method, pp. 97\u2013120. Elsevier (2000)","DOI":"10.1016\/B978-044450556-9\/50065-4"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-642-33666-9_27","volume-title":"Model Driven Engineering Languages and Systems","author":"M. Kuhlmann","year":"2012","unstructured":"Kuhlmann, M., Gogolla, M.: From UML and OCL to relational logic and back. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol.\u00a07590, pp. 415\u2013431. Springer, Heidelberg (2012)"},{"key":"11_CR25","unstructured":"Lund, M.S.: Operational Analysis of Sequence Diagram Specifications. PhD thesis (2007)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Lund, M.S., St\u00f8len, K.: Deriving tests from UML 2.0 sequence diagrams with neg and assert. In: Intl. Workshop on Automation of Software Test, AST 2006, pp. 22\u201328. ACM (2006)","DOI":"10.1145\/1138929.1138934"},{"key":"11_CR27","unstructured":"MDT-OCL-Team. MDT OCL (2008), http:\/\/www.eclipse.org\/modeling\/mdt\/?project=ocl\/"},{"key":"11_CR28","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science\u00a096, 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"11_CR29","unstructured":"Meseguer, J.: 20 years of rewriting logic. Technical report, University of Illinois at Urbana-Champaign (2012), http:\/\/hdl.handle.net\/2142\/32096"},{"issue":"2","key":"11_CR30","doi-asserted-by":"publisher","first-page":"136","DOI":"10.5381\/jot.2009.8.2.a2","volume":"8","author":"F. Mokhati","year":"2009","unstructured":"Mokhati, F., Badri, M.: Generating Maude Specifications from UML Use Case Diagrams. Journal of Object Technology\u00a08(2), 136\u2013319 (2009)","journal-title":"Journal of Object Technology"},{"key":"11_CR31","unstructured":"Object\u00a0Management Group. OMG unified modeling language (OMG UML), superstructure, v2.1.2 (formal\/2007-11-02) (2007), http:\/\/atenea.lcc.uma.es\/index.php\/Main_Page\/Resources\/MaudeMM"},{"key":"11_CR32","unstructured":"Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: A metamodel for Maude, http:\/\/atenea.lcc.uma.es\/index.php\/Main_Page\/Resources\/MaudeMM"},{"issue":"11-12","key":"11_CR33","doi-asserted-by":"publisher","first-page":"778","DOI":"10.1177\/0037549709341635","volume":"85","author":"J.E. Rivera","year":"2009","unstructured":"Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: Formal Specification and Analysis of Domain Specific Models Using Maude. Simulation\u00a085(11-12), 778\u2013792 (2009)","journal-title":"Simulation"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: A Graphical Approach for Modeling Time-Dependent Behavior of DSLs. In: 2009 IEEE Symposium on Visual Languages and Human-Centric Computing, VL\/HCC 2009, pp. 51\u201355. IEEE (2009)","DOI":"10.1109\/VLHCC.2009.5295300"},{"key":"11_CR35","unstructured":"Rold\u00e1n, M., Dur\u00e1n, F.: Dynamic validation of OCL constraints with mOdCL. ECEASST\u00a044 (2011)"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of UML models. In: Design, Automation and Test in Europe, DATE 2011, pp. 1077\u20131082. IEEE (2011)","DOI":"10.1109\/DATE.2011.5763177"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL models using boolean satisfiability. In: Design, Automation and Test in Europe, DATE 2010, pp. 1341\u20131344. IEEE (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"11_CR38","unstructured":"Software Technology Group. DresdenOCL, http:\/\/www.dresden-ocl.org\/"},{"issue":"5","key":"11_CR39","first-page":"1","volume":"10","author":"J. Troya","year":"2011","unstructured":"Troya, J., Vallecillo, A.: A rewriting logic semantics for ATL. Journal of Object Technology\u00a010(5), 1\u201329 (2011)","journal-title":"Journal of Object Technology"},{"key":"11_CR40","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley (2003)"},{"key":"11_CR41","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1016\/S0304-3975(01)00367-X","volume":"285","author":"M. Wirsing","year":"2001","unstructured":"Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. Theoretical Computer Science\u00a0285, 519\u2013560 (2001)","journal-title":"Theoretical Computer Science"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Zhang, C., Duan, Z.: Specification and verification of UML 2.0 sequence diagrams using event deterministic finite automata. In: Fifth Intl. Conf. on Secure Software Integration and Reliability Improvement, SSIRI 2011, pp. 41\u201346. IEEE (2011)","DOI":"10.3724\/SP.J.1001.2011.04005"}],"container-title":["Lecture Notes in Computer Science","Specification, Algebra, and Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54624-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T02:26:21Z","timestamp":1648434381000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54624-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642546235","9783642546242"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54624-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}