{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T17:42:07Z","timestamp":1762623727208},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496640"},{"type":"electronic","value":"9783662496657"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49665-7_18","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T04:09:42Z","timestamp":1458533382000},"page":"305-322","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Statistical Model Checking of e-Motions Domain-Specific Modeling Languages"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[]},{"given":"Antonio","family":"Moreno-Delgado","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9 M.","family":"\u00c1lvarez-Palomo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Agha, G., Greenwald, M., Gunter, C.A., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of DOS using probabilistic rewrite theories. In: Proceedings of FCS (2005)"},{"issue":"2","key":"18_CR2","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"Gul Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. In: Proceedings of the QAPL, ENTCS, vol. 153, pp. 213\u2013239 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III: Verification and Control","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996)"},{"key":"18_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. 4961, pp. 377\u2013391. Springer, Heidelberg (2008)"},{"key":"18_CR6","unstructured":"Boronat, A., Meseguer, J.: MOMENT2: EMF model transformations in Maude. In: Proceedings of JISBD, pp. 178\u2013179 (2009)"},{"issue":"1\u20132","key":"18_CR7","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoret. Comput. Sci. 236(1\u20132), 35\u2013132 (2000)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-34005-5_7","volume-title":"Rewriting Logic and Its Applications","author":"R Bruni","year":"2012","unstructured":"Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: Modelling and analyzing adaptive self-assembly strategies with Maude. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 118\u2013138. Springer, Heidelberg (2012)"},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.85.1","volume":"85","author":"PE Bulychev","year":"2012","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. EPTCS 85, 1\u201316 (2012). Proceedings of QAPL","journal-title":"EPTCS"},{"issue":"2","key":"18_CR10","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M Clavel","year":"2001","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. Theoret. Comput. Sci. 285(2), 187\u2013243 (2001)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude","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. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"issue":"1","key":"18_CR12","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10270-012-0242-3","volume":"13","author":"J Lara de","year":"2014","unstructured":"de Lara, J., Guerra, E., Boronat, A., Heckel, R., Torrini, P.: Domain-specific discrete event modelling and simulation using graph transformation. Softw. Syst. Model. 13(1), 209\u2013238 (2014)","journal-title":"Softw. Syst. Model."},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45923-5_12","volume-title":"Fundamental Approaches to Software Engineering","author":"J Lara de","year":"2002","unstructured":"de Lara, J., Vangheluwe, H.: AToM: a tool for multi-formalism and meta-modelling. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 174\u2013188. Springer, Heidelberg (2002)"},{"issue":"1\u20132","key":"18_CR14","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10990-008-9028-2","volume":"21","author":"F Dur\u00e1n","year":"2008","unstructured":"Dur\u00e1n, F., Lucas, S., March\u00e9, C., Meseguer, J., Urbain, X.: Proving operational termination of membership equational programs. Higher-Order Symbol. Comput. 21(1\u20132), 59\u201388 (2008)","journal-title":"Higher-Order Symbol. Comput."},{"issue":"7\u20138","key":"18_CR15","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebr. Program. 81(7\u20138), 816\u2013850 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-28872-2_6","volume-title":"Fundamental Approaches to Software Engineering","author":"J Eckhardt","year":"2012","unstructured":"Eckhardt, J., M\u00fchlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering. LNCS, vol. 7212, pp. 78\u201393. Springer, Heidelberg (2012)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-30203-2_16","volume-title":"Graph Transformations","author":"R Heckel","year":"2004","unstructured":"Heckel, R., Lajios, G., Menge, S.: Stochastic graph transformation systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 210\u2013225. Springer, Heidelberg (2004)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-38592-6_13","volume-title":"Formal Techniques for Distributed Systems","author":"T Isenberg","year":"2013","unstructured":"Isenberg, T., Steenken, D., Wehrheim, H.: Bounded model checking of graph transformation systems via SMT solving. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 178\u2013192. Springer, Heidelberg (2013)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-77966-7_9","volume-title":"Hardware and Software: Verification and Testing","author":"DN Jansen","year":"2008","unstructured":"Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 69\u201385. Springer, Heidelberg (2008)"},{"key":"18_CR20","doi-asserted-by":"publisher","DOI":"10.1002\/9780470249260","volume-title":"Domain-Specific Modeling: Enabling Full Code Generation","author":"S Kelly","year":"2008","unstructured":"Kelly, S., Tolvanen, J.-P.: Domain-Specific Modeling: Enabling Full Code Generation. Wiley, New York (2008)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-47884-1_16","volume-title":"Integrated Formal Methods","author":"B Caskurlu","year":"2002","unstructured":"Caskurlu, B.: Model driven engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286\u2013298. Springer, Heidelberg (2002)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52\u201366. Springer, Heidelberg (2002)"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"issue":"1","key":"18_CR24","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. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR25","unstructured":"Meta object facility (MOF) core specification, Version 2.4.1 (2013)"},{"key":"18_CR26","unstructured":"Moreno-Delgado, A., Dur\u00e1n, F.: The movie database case: a solution using the Maude-based e-Motions tool. In: 7th Transformation Tool Contest (TTC), vol. 1305, pp. 116\u2013124. CEUR Workshop Proceedings (2014)"},{"issue":"1\u20132","key":"18_CR27","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order Symbol. Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"Higher-Order Symbol. Comput."},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-25959-6_40","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"A Rensink","year":"2004","unstructured":"Rensink, A.: The GROOVE simulator: a\u00a0tool for state space generation. In: Pfaltz, J.L., Nagl, M., B\u00f6hlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479\u2013485. Springer, Heidelberg (2004)"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: A graphical approach for modeling time-dependent behavior of DSLs. In: Proceedings of VL\/HCC, pp. 51\u201355. IEEE (2009)","DOI":"10.1109\/VLHCC.2009.5295300"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-16310-4_12","volume-title":"Rewriting Logic and Its Applications","author":"JE Rivera","year":"2010","unstructured":"Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: On the behavioral semantics of real-time domain specific visual languages. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 174\u2013190. Springer, Heidelberg (2010)"},{"issue":"11\/12","key":"18_CR31","doi-asserted-by":"publisher","first-page":"778","DOI":"10.1177\/0037549709341635","volume":"85","author":"JE Rivera","year":"2009","unstructured":"Rivera, J.E., Vallecillo, A., Dur\u00e1n, F.: Formal specification and analysis of domain specific languages using Maude. Simulation 85(11\/12), 778\u2013792 (2009)","journal-title":"Simulation"},{"issue":"9","key":"18_CR32","doi-asserted-by":"publisher","first-page":"187","DOI":"10.5381\/jot.2007.6.9.a10","volume":"6","author":"JR Romero","year":"2007","unstructured":"Romero, J.R., Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: Formal and tool support for model driven engineering with Maude. J. Object Technol. 6(9), 187\u2013207 (2007)","journal-title":"J. Object Technol."},{"volume-title":"Handbook of Graph Grammars and Computing by Graph Transformations: Volume 1 Foundations","year":"1997","key":"18_CR33","unstructured":"Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformations: Volume 1 Foundations. World Scientific, River Edge (1997)"},{"key":"18_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-45221-8_8","volume-title":"\u00abUML\u00bb 2003 - The Unified Modeling Language. Modeling Languages and Applications","author":"\u00c1 Schmidt","year":"2003","unstructured":"Schmidt, \u00c1., Varr\u00f3, D.: CheckVML: a tool for model checking visual modeling languages. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 92\u201395. Springer, Heidelberg (2003)"},{"key":"18_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: VeStA: a statistical model-checker and analyzer for probabilistic systems. In: Proceedings of QEST, pp. 251\u2013252. IEEE (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"18_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-540-25959-6_35","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"G Taentzer","year":"2004","unstructured":"Taentzer, G.: AGG: a\u00a0graph transformation environment for modeling and validation of software. In: Pfaltz, J.L., Nagl, M., B\u00f6hlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446\u2013453. Springer, Heidelberg (2004)"},{"key":"18_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-12029-9_11","volume-title":"Fundamental Approaches to Software Engineering","author":"P Torrini","year":"2010","unstructured":"Torrini, P., Heckel, R., R\u00e1th, I.: Stochastic simulation of graph transformation systems. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 154\u2013157. Springer, Heidelberg (2010)"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429\u2013433. Springer, Heidelberg (2005)"},{"key":"18_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002)"},{"key":"18_CR41","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.asoc.2014.06.055","volume":"24","author":"R Yousefian","year":"2014","unstructured":"Yousefian, R., Rafe, V., Rahmani, M.: A heuristic solution for model checking graph transformation systems. Appl. Soft Comput. 24, 169\u2013180 (2014)","journal-title":"Appl. Soft Comput."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49665-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T21:11:28Z","timestamp":1584997888000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}