- -

Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: Chapter2-author.pdf
Tamaño: 612.1Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Combining runtime ...
Tamaño: 737.8Kb
Formato: PDF
Solicitar una copia al autor
dc.contributor.author Alpuente Frasnedo, María es_ES
dc.contributor.author Ballis, Demis es_ES
dc.contributor.author Frechina Navarro, Francisco es_ES
dc.contributor.author Sapiña Sanchis, Julia es_ES
dc.contributor.editor Springer-Verlag es_ES
dc.date.accessioned 2016-02-22T13:31:20Z
dc.date.available 2016-02-22T13:31:20Z
dc.date.issued 2015-08
dc.identifier.isbn 978-3-319-23164-8
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/10251/61075
dc.description The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-23165-5_3 es_ES
dc.description.abstract This paper introduces the idea of using assertion checking for enhancing the dynamic slicing of Maude computation traces. Since trace slicing can greatly simplify the size and complexity of the analyzed traces, our methodology can be useful for improving the diagnosis of erroneous Maude programs. The proposed methodology is based on (i) a logical notation for specifying two types of user-defined assertions that are imposed on execution runs: functional assertions and system assertions; (ii) a runtime checking technique that dynamically tests the assertions and is provably safe in the sense that all errors flagged are definite violations of the specifications; and (iii) a mechanism based on equational least general generalization that automatically derives accurate criteria for slicing from falsified assertions. es_ES
dc.description.sponsorship This work has been partially supported by the EU (FEDER) and the Spanish MINECO project ref. TIN2013-45732-C4-01 (DAMAS), and by Generalitat Valenciana ref. PROMETEOII/2015/013 (SmartLogic). F. Frechina was supported by FPU-ME grant AP2010-5681, and J. Sapiña was supported by FPI-UPV grant SP2013-0083. es_ES
dc.language Inglés es_ES
dc.relation.ispartof Logic, Rewriting, and Concurrency. Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;9200
dc.rights Reserva de todos los derechos es_ES
dc.subject Rewriting Logic es_ES
dc.subject Error Diagnosis es_ES
dc.subject Assertion Chackin es_ES
dc.subject Automated Slicing es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis es_ES
dc.type Capítulo de libro es_ES
dc.identifier.doi 10.1007/978-3-319-23165-5_3
dc.relation.projectID info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/ME//AP2010-5681/ES/AP2010-5681/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/UPV//FPI%2FSP2013-0083/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Alpuente Frasnedo, M.; Ballis, D.; Frechina Navarro, F.; Sapiña Sanchis, J. (2015). Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis. En Logic, Rewriting, and Concurrency. Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday. 72-96. https://doi.org/10.1007/978-3-319-23165-5_3 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion http://link.springer.com/chapter/10.1007/978-3-319-23165-5_3 es_ES
dc.description.upvformatpinicio 72 es_ES
dc.description.upvformatpfin 96 es_ES
dc.relation.senia 300396 es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder Ministerio de Economía y Competitividad es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Universitat Politècnica de València es_ES
dc.contributor.funder Ministerio de Educación es_ES
dc.description.references Alpuente, M., Ballis, D., Espert, J., Romero, D.: Backward trace slicing for rewriting logic theories. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 34–48. Springer, Heidelberg (2011) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Backward trace slicing for conditional rewrite theories. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 62–76. Springer, Heidelberg (2012) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Julienne: a trace slicer for conditional rewrite theories. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 28–32. Springer, Heidelberg (2012) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Using conditional trace slicing for improving Maude programs. Sci. Comput. Program. 80, Part B:385–415 (2014) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Slicing-based trace analysis of rewriting logic specifications with $$I$$ Julienne. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 121–124. Springer, Heidelberg (2013) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Inspecting rewriting logic computations (in a Parametric and Stepwise Way). In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 229–255. Springer, Heidelberg (2014) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Debugging Maude programs via runtime assertion checking and trace slicing. Technical report, Department of Computer Systems and Computation, Universitat Politècnica de València (2015). http://safe-tools.dsic.upv.es/abets/abets-tr.pdf es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Exploring conditional rewriting logic computations. J. Symbolic Comput. 69, 3–39 (2015) es_ES
dc.description.references Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98–136 (2014) es_ES
dc.description.references Baader, F., Snyder, W.: Unification Theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 447–533. Elsevier Science (2001) es_ES
dc.description.references Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1–3), 386–414 (2006) es_ES
dc.description.references Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Softw. Eng. Notes 31(3), 25–37 (2006) es_ES
dc.description.references Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS. Springer, Heidelberg (2007) es_ES
dc.description.references Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.6). Technical report, SRI International Computer Science Laboratory (2011). http://maude.cs.uiuc.edu/maude2-manual/ es_ES
dc.description.references Durán, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010) es_ES
dc.description.references Durán, F., Roldán, M., Vallecillo, A.: Invariant-driven strategies for Maude. Electron. Notes Theor. Comput. Sci. 124(2), 17–28 (2005) es_ES
dc.description.references Goguen, J.A., Meseguer, J.: Equality, types, modules, and (why not?) generics for logic programming. J. Logic Program. 1(2), 179–210 (1984) es_ES
dc.description.references Goguen, J.A., Meseguer, J.: Unifying functional, object-oriented and relational programming with logical semantics. In: Agha, G., Wegner, P., Yonezawa, A. (eds.), Research Directions in Object-Oriented Programming, pp. 417–478. The MIT Press (1987) es_ES
dc.description.references Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.), Handbook of Logic in Computer Science, vol. I, pp. 1–112. Oxford University Press (1992) es_ES
dc.description.references Korel, B., Laski, J.: Dynamic program slicing. Inf. Process. Lett. 29(3), 155–163 (1988) es_ES
dc.description.references Lassez, J.L., Maher, M.J., Marriott, K.: Unification Revisited. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 587–625. Morgan Kaufmann, Los Altos, California (1988) es_ES
dc.description.references Leavens, G.T., Cheon, Y.: Design by Contract with JML (2005). http://www.eecs.ucf.edu/ leavens/JML/jmldbc.pdf es_ES
dc.description.references Martí-Oliet, N., Palomino, M., Verdejo, A.: Rewriting logic bibliography by topic: 1990–2011. J. Logic Algebraic Program. 81(7–8), 782–815 (2012) es_ES
dc.description.references Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73–155 (1992) es_ES
dc.description.references Meseguer, J.: Multiparadigm logic programming. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 158–200. Springer, Heidelberg (1992) es_ES
dc.description.references Rocha, C., Meseguer, J., Muñoz, C.: Rewriting modulo SMT and open system analysis. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 247–262. Springer, Heidelberg (2014) es_ES
dc.description.references Roşu, G.: From Rewriting Logic, to Programming Language Semantics, to Program Verification. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C., (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 598–616. Springer, Heidelberg (2015) es_ES
dc.description.references Roldán, M., Durán, F., Vallecillo, A.: Invariant-driven specifications in Maude. Sci. Comput. Program. 74(10), 812–835 (2009) es_ES
dc.description.references TeReSe. Term Rewriting Systems. Cambridge University Press (2003) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem