Suchergebnisse

[EN] Program transformation is widely used for producing correct mutations of a given program so as to satisfy the user's intent that can be expressed by means of some sort of specification (e.g. logical assertions, functional specifications, reference implementations, summaries, examples). This paper describes an automated correction methodology for Maude programs that is based on program transformation and can be used to enforce a safety policy, given by a set A of system assertions, in a Maude program R that might disprove some of the assertions. The outcome of the technique is a safe program refinement R' of R in which every computation is a good run, i.e., it satisfies the assertions in A. Furthermore, the transformation ensures that no good run of R is removed from R'. Advantages of this correction methodology can be summarized as follows. A fully automatic program transformation featuring both program diagnosis and repair that preserves all executability requirements. A simple logical notation to declaratively express invariant properties and other safety constraints through assertions. No dynamic information is required to infer program fixes: the methodology is static and does not need to collect any error symptom at runtime. ; This work has been partially supported by the EU (FEDER) and the Spanish MINECO under grant RTI2018-094403-B-C32, and by Generalitat Valenciana under grant PROMETEO/2019/098. ; Alpuente Frasnedo, M.; Ballis, D.; Sapiña-Sanchis, J. (2019). Imposing Assertions in Maude via Program Transformation. MethodsX. 6:2577-2583. https://doi.org/10.1016/j.mex.2019.10.035 ; S ; 2577 ; 2583 ; 6

[EN] This paper develops a Rewriting Logic framework for the automatic specification and verification of Web applications that considers the critical aspects of concurrent Web interactions, browser navigation features (e.g., forward/back-ward navigation, page refresh, and new window/tab opening), and Web script evaluation. By encompassing the main features of the most popular Web scripting languages (e.g., PHP, ASP, and Java Servlets), our scripting language is powerful enough to model the dynamics of complex Web applications, where the interactions among Web servers and Web browsers are formalized through a landmark communicating protocol that abstracts HTTP. We provide a detailed characterization of browser actions via rewrite rules and show how our models can be naturally model-checked by using the Linear Temporal Logic of Rewriting (LTLR), which is a Linear Temporal Logic that is specifically designed for model-checking rewrite theories. The framework has been completely implemented in Maude, and we report on some successful experiments that we conducted using the Maude LTLR model-checker. ; This work has been partially supported by the EU (FEDER) and the Spanish MEC project ref. TIN2010-21062-C02-02, and by Generalitat Valenciana ref. PROMETE02011/052. This work was carried out during the tenure by Demis Ballis of an ERCIM "Alain Bensoussan" Postdoctoral Fellowship. The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement no 246016. Daniel Romero was partially supported by FPI-MEC grant BES-2008-004860. ; Alpuente Frasnedo, M.; Ballis, D.; Romero, DO. (2014). A rewriting logic approach to the formal specification and verification of web applications. Science of Computer Programming. 81:79-107. https://doi.org/10.1016/j.scico.2013.07.014 ; S ; 79 ; 107 ; 81

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-54624-2_12 ; Trace inspection is concerned with techniques that allow the trace content to be searched for specific components. This paper presents a rich and highly dynamic, parameterized technique for the trace inspection of Rewriting Logic theories that allows the non-deterministic execution of a given unconditional rewrite theory to be followed up in different ways. Using this technique, an analyst can browse, slice, filter, or search the traces as they come to life during the program execution. Starting from a selected state in the computation tree, the navigation of the trace is driven by a user-defined, inspection criterion that specifies the required exploration mode. By selecting different inspection criteria, one can automatically derive a family of practical algorithms such as program steppers and more sophisticated dynamic trace slicers that facilitate the dynamic detection of control and data dependencies across the computation tree. Our methodology, which is implemented in the Anima graphical tool, allows users to capture the impact of a given criterion thereby facilitating the detection of improper program behaviors. ; This work has been partially supported by the EU (FEDER), the Spanish MEC project ref. TIN2010-21062-C02-02, the Spanish MICINN complementary action ref. TIN2009-07495-E, and by Generalitat Valenciana ref. PROMETEO2011/052. This work was carried out during the tenure of D. Ballis' ERCIM "Alain Bensoussan "Postdoctoral Fellowship. The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement n. 246016. F. Frechina was supported by FPU-ME grant AP2010-5681. ; Alpuente Frasnedo, M.; Ballis, D.; Frechina, F.; Sapiña Sanchis, J. (2014). Inspecting rewriting logic computations (in a parametric and stepwise way). En Specification, algebra, and software: essays dedicated to Kokichi Futatsugi. Springer Verlag (Germany). ...

[EN] Understanding the behavior of software is important for the existing software to be improved. In this paper, we present a trace slicing technique that is suitable for analyzing complex, textually-large computations in rewriting logic, which is a general framework efficiently implemented in the Maude language that seamlessly unifies a wide variety of logics and models of concurrency. Given a Maude execution trace T and a slicing criterion for the trace (i.e., a piece of information that we want to observe in the final computation state), we traverse T from back to front and the backward dependence of the observed information is incrementally computed at each execution step. At the end of the traversal, a simplified trace slice is obtained by filtering out all the irrelevant data that do not impact on the data of interest. By narrowing the size of the trace, the slicing technique favors better inspection and debugging activities since most tedious and irrelevant inspections that are routinely performed during diagnosis and bug localization can be eliminated automatically. Moreover, cutting down the execution trace can expose opportunities for further improvement, which we illustrate by means of several examples that we execute by using iJulienne, a trace slicer that implements our conditional slicing technique and is endowed with a trace querying mechanism that increases flexibility and reduction power. ; This work has been partially supported by the EU (FEDER) and the Spanish MEC project ref. TIN2010-21062-C02-02, and by Generalitat Valenciana ref. PROMETEO2011/052. This work was carried out during the tenure of D. Ballis' ERCIM "Alain Bensoussan" Postdoctoral Fellowship. The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement No. 246016. F. Frechina was supported by FPU-ME grant AP2010-5681 and D. Romero by FPI-MEC grant BES-2008-004860. ; Alpuente Frasnedo, M.; Ballis, D.; Frechina, F.; Romero, DO. (2014). Using ...

[EN] The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order-sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of different, increasingly efficient formulations of the homeomorphic embedding relation modulo axioms that we implement in Maude. Our experimental results show that the most efficient version indeed pays off in practice. ; M. Alpuente and S. Escobar have been partially supported by the EU (FEDER) and the Spanish MCIU under grant RTI2018-094403-B-C32, by the Spanish Generalitat Valenciana under grant PROMETEO/2019/098, and by the European Union's Horizon 2020 research and innovation programme under grant agreement No. 952215 (TAILOR). J. Meseguer has been supported by NRL under contract number N00173-17-1-G002. A. Cuenca-Ortega has been supported by the SENESCYT, Ecuador (scholarship program 2013). ; Alpuente Frasnedo, M.; Cuenca-Ortega, A.; Escobar Román, S.; Meseguer, J. (2020). Order-sorted Homeomorphic Embedding modulo Combinations of Associativity and/or Commutativity Axioms. Fundamenta Informaticae. 177(3-4):297-329. https://doi.org/10.3233/FI-2020-1991 ; S ; 297 ; 329 ; 177 ; 3-4

[EN] Trace exploration is concerned with techniques that allow computation traces to be dynamically searched for specific contents. Depending on whether the exploration is carried backward or forward, trace exploration techniques allow provenance tracking or impact tracking to be done. The aim of provenance tracking is to show how (parts of) a program output depends on (parts of) its input and to help estimate which input data need to be modified to accomplish a change in the outcome. The aim of impact tracking is to identify the scope and potential consequences of changing the program input. Rewriting Logic (RWL) is a logic of change that supplements (an extension of) the equational logic by adding rewrite rules that are used to describe (nondeterministic) transitions between states. In this paper, we present a rich and highly dynamic, parameterized technique for the forward inspection of RWL computations that allows the nondeterministic execution of a given conditional rewrite theory to be followed up in different ways. With this technique, an analyst can browse, slice, filter, or search the traces as they come to life during the program execution. The navigation of the trace is driven by a user-defined, inspection criterion that specifies the required exploration mode. By selecting different inspection criteria, one can automatically derive a family of practical algorithms such as program steppers and more sophisticated ; This work has been partially supported by the EU (FEDER) and the Spanish MEC project Ref. TIN2010-21062-C02-02, the Spanish MICINN complementary action Ref. TIN2009-07495-E, and by Generalitat Valenciana Ref. PROMETEO2011/052. This work was carried out during the tenure of D. Ballis' ERCIM "Alain Bensoussan" Postdoctoral Fellowship. The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement N. 246016. F. Frechina was supported by FPU-ME grant AP2010-5681, and J. Sapina was supported by FPI-UPV grant ...

[EN] Keeping XML data in a consistent state w.r.t. both structure and content is a burdensome task. To maintain the consistency of ever-larger, complex XML repositories, suitable mechanisms that are able to x every possible inconsistency are needed. In this article, we present a methodology for semi-automatically repairing faulty XML repositories that can be integrated on top of an existing rewriting-based veri cation engine. As a formal basis for representing consistency criteria, we use a rule-based description formalism that is realized in the language Maude. Then, starting from a categorization of the kinds of errors that can be found during the veri cation process, we formulate a stepwise transformation procedure that achieves correctness and completeness of the XML repository w.r.t. its Maude formal speci cation while strictly observing the structure of the XML documents. With the aim of increasing the level of automation of our repair methodology, we also de ne two correction strategies and two completion strategies that reduce either the amount of information to be changed or the number of repair actions to be executed in order to deliver an XML repository that is both correct and complete. Finally, we describe a prototype implementation of the repairing tool, which we use for an experimental evaluation of our method with good results. ©2013 Elsevier Inc.All rights reserved. ; This work has been partially supported by the EU (FEDER) and the Spanish MEC project ref. TIN2010-21062-C02-02, and by Generalitat Valenciana ref. PROMETEO2011/052. This work was carried out during the tenure of D. Ballis' ERCIM "Alain Bensoussan" Postdoctoral Fellowship. The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007–2013) under grant agreement n. 246016. F. Frechina was supported by FPU-ME grant AP2010-5681 and D. Romero by FPI-MEC grant BES-2008-004860 We would like to thank the anonymous reviewers for their helpful comments. ; Alpuente Frasnedo, M.; ...