- -

Verificación de aplicaciones web dinámicas con Web-TLR

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Verificación de aplicaciones web dinámicas con Web-TLR

Show simple item record

Files in this item

dc.contributor.advisor Alpuente Frasnedo, María es_ES
dc.contributor.author Espert Real, Javier es_ES
dc.date.accessioned 2011-07-20T11:23:02Z
dc.date.available 2011-07-20T11:23:02Z
dc.date.created 2011-07-13
dc.date.issued 2011-07-20
dc.identifier.uri http://hdl.handle.net/10251/11219
dc.description.abstract Web-TLR is a software tool designed for model-checking Web applications that is based on rewriting logic. Web applications are expressed as rewrite theories that can be formally verified by using the Maude built-in LTLR model-checker. Whenever a property is refuted, it produces a counterexample trace that underlies the failing model checking computation. However, the analysis (or even the simple inspection) of large counterexamples may prove to be unfeasible due to the size and complexity of the traces under examination. This work aims to improve the understandability of the counterexamples generated by Web-TLR by developing an integrated framework for debugging Web applications that integrates a trace-slicing technique for rewriting logic theories that is particularly tailored to Web-TLR. The verification environment is also provided with a user-friendly, graphical Web interface that shields the user from unnecessary information. Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simpli es the traces by detecting control and data dependencies, and dropping useless data that do not infuence the final result. Our methodology is particularly suitable for analyzing complex, textually-large system computations such as those delivered as counter-example traces by Maude model-checkers. The slicing facility implemented in Web-TLR allows the user to select the pieces of information that she is interested into by means of a suitable pattern-matching language supported by wildcards. The selected information is then traced back through inverse rewrite sequences. The slicing process drastically simpli es the computation trace by dropping useless data that do not influence the nal result. By using this facility, the Web engineer can focus on the relevant fragments of the failing application, which greatly reduces the manual debugging e ort and also decreases the number of iterative verfications. es_ES
dc.format.extent 88 es_ES
dc.language Inglés es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Model checking es_ES
dc.subject Trace slicing es_ES
dc.subject Web verification es_ES
dc.subject Rewriting logic es_ES
dc.subject Counterexample generation es_ES
dc.subject Linear temporal logic of rewriting es_ES
dc.subject Web debugging es_ES
dc.subject.other Ingeniería Informática-Enginyeria Informàtica es_ES
dc.title Verificación de aplicaciones web dinámicas con Web-TLR es_ES
dc.type Proyecto/Trabajo fin de carrera/grado es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica es_ES
dc.description.bibliographicCitation Espert Real, J. (2011). Verificación de aplicaciones web dinámicas con Web-TLR. http://hdl.handle.net/10251/11219. es_ES
dc.description.accrualMethod Archivo delegado es_ES


This item appears in the following Collection(s)

Show simple item record