1,721,002 research outputs found
Backward Trace Slicing for Rewriting Logic Theories -Technical report -
Full text linkTrace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. 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 simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence 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.Alpuente Frasnedo, M.; Ballis, D.; Espert, J.; Romero, D. (2011). Backward Trace Slicing for Rewriting Logic Theories -Technical report -. https://riunet.upv.es/handle/10251/1076
Imposing assertions in Maude via program transformation
Full text link[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.035S25772583
Optimizing Maude Programs via Program Specialization
No full textWe develop an automated specialization framework for rewrite theories that model concurrent systems. A rewrite theory R= (Σ, E⊎ B, R) consists of two main components: an order-sorted equational theory E= (Σ, E⊎ B) that defines the system states as terms of an algebraic data type and a term rewriting system R that models the concurrent evolution of the system as state transitions. Our main idea is to partially evaluate the underlying equational theory E to the specific calls required by the rewrite rules of R in order to make the system computations more efficient. The specialization transformation relies on folding variant narrowing, which is the symbolic operational engine of Maude’s equational theories. We provide three instances of our specialization scheme that support distinct classes of theories that are relevant for many applications. The effectiveness of our method is finally demonstrated in some specialization examples
On Unfolding Completeness for Rewriting Logic Theories
Full text linkMany transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of the original theory.Alpuente Frasnedo, M.; Baggi, M.; Ballis, D.; Falaschi, M. (2010). On Unfolding Completeness for Rewriting Logic Theories. https://riunet.upv.es/handle/10251/863
A Rewriting-Based Framework for Web Sites Verification
No full textIn this paper, we develop a framework for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. First, we provide a rewriting-based, formal specification language which allows us to define syntactic as well as semantic properties of the Web site. Then, we formalize a verification technique which obtains the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete information and/or missing pages. Our methodology is based on a novel rewriting-based technique, called partial rewriting, in which the traditional pattern matching mechanism is replaced by tree simulation, a suitable technique for recognizing patterns inside semistructured documents. The framework has been implemented in the prototype Web verification system Verdi which is publicly available
Optimization of rewrite theories by equational partial evaluation
Full text linkIn this paper, we develop an automated optimization framework for rewrite theories that supports sorts, subsort overloading, equations and algebraic axioms with free/non-free constructors, and rewrite rules modeling concurrent system transitions whose state structure is defined by means of the equations. The main idea of the framework is to make the system computations more efficient by partially evaluating the equations to the specific calls that are required by the transition rules. This can be particularly useful for automatically optimizing rewrite theories that contain overly general equational theories which perform unnecessary and costly computations involving pattern matching and/or unification modulo equations and axioms. The transformation is based on a suitable unfolding operator parameter that relies on the symbolic operational engine of Maude's equational theories, called folding variant narrowing, together with a generic abstraction operator. Depending on the properties of the rewrite theory, the unfolding and abstraction operators must be fine-tuned to achieve the biggest optimization possible while ensuring termination and total correctness of the transformation. We formalize two instances of our scheme for the case when the rewrite theory either has an infinite number of most general variants or a finite number of most general variants. Finally, we discuss some experimental results which demonstrate that the proposed optimization technique pays off in practice
Symbolic Specialization of Rewriting Logic Theories with Presto
No full textThis paper introduces Presto, a symbolic partial evaluator for Maude's rewriting logic theories that can improve system analysis and verification. In Presto, the automated optimization of a conditional rewrite theory R (whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of R, an underlying, companion equational logic theory E that specifies the algebraic structure of the system states of R. This can be particularly useful for specializing an overly general equational theory E whose operators may obey complex combinations of associativity, commutativity, and/or identity axioms, when being plugged into a host rewrite theory R as happens, for instance, in protocol analysis, where sophisticated equational theories for cryptography are used. Presto implements different unfolding operators that are based on folding variant narrowing (the symbolic engine of Maude's equational theories). When combined with an appropriate abstraction algorithm, they allow the specialization to be adapted to the theory termination behavior and bring significant improvement while ensuring strong correctness and termination of the specialization. We demonstrate the effectiveness of Presto in several examples of protocol analysis where it achieves a significant speed-up. Actually, the transformation provided by Presto may cut down an infinite folding variant narrowing space to a finite one, and moreover, some of the costly algebraic axioms and rule conditions may be eliminated as well. As far as we know, this is the first partial evaluator for Maude that respects the semantics of functional, logic, concurrent, and object-oriented computations
Variant-Based Equational Anti-unification
No full textThe dual of most general equational unifiers is that of least general equational anti-unifiers, i.e., most specific anti-instances modulo equations. This work aims to provide a general mechanism for equational anti-unification that leverages the recent advances in variant-based symbolic computation in Maude. Symbolic computation in Maude equational theories is based on folding variant narrowing (FVN), a narrowing strategy that efficiently computes the equational variants of a term (i.e., the irreducible forms of all of its substitution instances). By relying on FVN, we provide an equational anti-unification algorithm that computes the least general anti-unifiers of a term in any equational theory E where the number of least general E-variants is finite for any given term
ccReact: a rewriting framework for the formal analysis of reaction systems
No full textReaction Systems (RSs) are a computational framework inspired by biochemical systems, where entities produced by reactions can enable or inhibit other reactions. RSs interact with the environment through a sequence of sets of entities called the context. In this work, we introduce ccReact, a novel interaction language for implementing and verifying RSs. ccReact extends the classical RS model by allowing the specification of recursive, nondeterministic, and conditional context sequences, thus enhancing the interactive capabilities of the models. We provide a rewriting logic (RL) semantics for ccReact, making it executable in the Maude system. We prove that our RL embedding is sound and complete, thereby offering a robust tool for analyzing RSs. Our methods enable various formal analysis techniques for RSs, including simulation of RSs interacting with ccReact processes, verification of reachability properties, model checking of temporal (LTL and CTL) formulas, and exploring the system evolution through a graphical tool to better understand its behavior. We apply our methods to analyze RSs from different domains, including computer science and biological systems. Notably, we examine a complex breast cancer case study, demonstrating that our analysis can suggest improvements to the administration of monoclonal antibody therapeutic treatments in certain scenarios
Safety enforcement via programmable strategies in Maude
No full textThis work aims to provide a general mechanism for safety enforcement in rewriting logic computations. Our technique relies on an assertion-guided model transformation that leverages the newly defined Maude strategy language for ensuring rich safety policies in non-deterministic programs. The transformed system is guaranteed to comply with user-defined invariants that are expressed in a strategy-based, pattern-matching logic, thus preventing the concurrent system to reach any unsafe states. The performance and scalability of the technique is empirically evaluated and benchmarked on a set of realistic programs
- …
