- -

Debugging Maude programs via runtime assertion checking and trace slicing

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Debugging Maude programs via runtime assertion checking and trace slicing

Show simple item record

Files in this item

dc.contributor.author Alpuente Frasnedo, María es_ES
dc.contributor.author Ballis, Demis es_ES
dc.contributor.author Frechina, F. es_ES
dc.contributor.author Sapiña-Sanchis, Julia es_ES
dc.date.accessioned 2017-05-15T11:02:41Z
dc.date.available 2017-05-15T11:02:41Z
dc.date.issued 2016-08
dc.identifier.issn 2352-2208
dc.identifier.uri http://hdl.handle.net/10251/81131
dc.description [EN] This is the author’s version of a work that was accepted for publication in <Journal title>. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Journal of Logical and Algebraic Methods in Programming, [VOL 85, ISSUE 5, (2016)] DOI 10.1016/j.jlamp.2016.03.001. es_ES
dc.description.abstract In this paper we propose a dynamic analysis methodology for improving the diagnosis of erroneous Maude programs. The key idea is to combine runtime checking and dynamic trace slicing for automatically catching errors at runtime while reducing the size and complexity of the erroneous traces to be analyzed (i.e., those leading to states failing to satisfy some of the assertions). First, we formalize a technique that is aimed at automatically detecting deviations of the program behavior (symptoms) with respect to two types of user-defined assertions: functional assertions and system assertions. The proposed dynamic checking is provably sound in the sense that all errors flagged are definitely violations of the specifications. Then, upon eventual assertion violations we generate accurate trace slices that help identify the cause of the error. Our methodology is based on (i) a logical notation for specifying assertions that are imposed on execution runs; (ii) a runtime checking technique that dynamically tests the assertions; and (iii) a mechanism based on (equational) least general generalization that automatically derives accurate criteria for slicing from falsified assertions. Finally, we report on an implementation of the proposed technique in the assertion-based, dynamic analyzer ABETS and show how the forward and backward tracking of asserted program properties leads to a thorough trace analysis algorithm that can be used for program diagnosis and debugging. © 2016 Elsevier Inc. All rights reserved. es_ES
dc.description.sponsorship This work has been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN2015-69175-C4-1-R and TIN2013-45732-C4-1-P, and by Generalitat Valenciana Ref. PROMETEOII/2015/013. F. Frechina was supported by FPU-ME grant AP2010-5681, and J. Sapiña was supported by FPI-UPV grant SP2013-0083 and mobility grant VIIT-3946.
dc.language Inglés es_ES
dc.publisher Elsevier es_ES
dc.relation MINECO/TIN2015-69175-C4-1-R es_ES
dc.relation GV/PROMETEOII/2015/013 es_ES
dc.relation MECD/FPU-ME/ AP2010-5681 es_ES
dc.relation UPV/FPI-UPV/ SP2013-0083 es_ES
dc.relation MINECO/TIN2013-45732-C4-1-P
dc.relation.ispartof Journal of Logical and Algebraic Methods in Programming es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Trace slicing es_ES
dc.subject Runtime checking es_ES
dc.subject Dynamic program slicing es_ES
dc.subject Program diagnosis and debugging es_ES
dc.subject Rewriting logic es_ES
dc.subject Maude es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Debugging Maude programs via runtime assertion checking and trace slicing es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1016/j.jlamp.2016.03.001
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.contributor.affiliation Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica es_ES
dc.description.bibliographicCitation Alpuente Frasnedo, M.; Ballis, D.; Frechina, F.; Sapiña-Sanchis, J. (2016). Debugging Maude programs via runtime assertion checking and trace slicing. Journal of Logical and Algebraic Methods in Programming. 85(5):707-736. doi:10.1016/j.jlamp.2016.03.001 es_ES
dc.description.accrualMethod Senia es_ES
dc.relation.publisherversion http://dx.doi.org/10.1016/j.jlamp.2016.03.001 es_ES
dc.description.upvformatpinicio 707 es_ES
dc.description.upvformatpfin 736 es_ES
dc.type.version info:eu repo/semantics/publishedVersion es_ES
dc.description.volume 85 es_ES
dc.description.issue 5 es_ES
dc.relation.senia 313951 es_ES
dc.contributor.funder Ministerio de Economía y Competitividad (MINECO)
dc.contributor.funder Generalitat Valenciana (GV)
dc.contributor.funder Ministerio de Educación (MECD)
dc.contributor.funder Universitat Politècnica de València (UPV)


This item appears in the following Collection(s)

Show simple item record