Navegación

Búsqueda

Búsqueda avanzada

Resultados de búsqueda para Maude

First steps towards a specification of Blockchain systems using Maude

This work presents a formal specification of the blockchain algorithm. We specify the consensus algorithm in rewriting logic and Maude. The fact that the specification is executable allows us to simulate and analyze it, with the goal of identifying potential weaknesses and testing new algorithms built on top of the existing infrastructure.

Autores: Francisco Durán / Antonio Moreno-Delgado / 
Palabras Clave: Blockchain - Maude - Rewriting Logic

Towards a Maude-based implementation of MultEcore multilevel modelling languages

MultEcore is a language and tool for the definition of domain-specific modelling languages following the multilevel modelling approach. This work presents some challenges towards the rewriting logic semantics of multilevel model hierarchies and multilevel coupled model transformations used to specify such languages. Although we briefly describe the specification of hierarchies and transformations, we will focus on the latest additions to the language, which allow the instantiation of the multilevel models with a language of choice, e.g., OCL or SML, for the specification and manipulation of values of objects’ attributes, and the use of nested and cross-level boxes for the specification of patterns in the rules. The executable specification can then be used for the simulation/execution of MultEcore models and their analysis using Maude formal tools.

Autores: Francisco Durán / Alejandro Rodríguez / 
Palabras Clave: Maude - MultEcore - multilevel modeling - Rewriting Logic

Variant-based Equational Unification under Constructor Symbols

Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. A narrowing-based equational unification algorithm relying on the concept of the variants of a term is available in the most recent version of Maude, version 3.0, which provides quite sophisticated unification features. A variant of a term t is a pair consisting of a substitution σ and the canonical form of tσ. Variant-based unification is decidable when the equational theory satisfies the finite variant property. However, this unification procedure does not take into account constructor symbols and, thus, may compute many more unifiers than the necessary or may not be able to stop immediately. In [1], we integrate the notion of constructor symbol into the variant-based unification algorithm. Our experiments on positive and negative unification problems show an impressive speedup.

Autores: Damián Aparicio-Sánchez / Santiago Escobar / Julia Sapiña / 
Palabras Clave: equational unification - Maude - Variants

Verification of ROS Navigation using Maude

The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The emph{Navigation Stack} stands out among the different libraries available in ROS. This library provides a set of reusable components that developers can use to build robots with autonomous navigation capabilities. This is a critical component, as navigation failures could have catastrophical consequences for applications like self-driving cars.Here we show our work on the verification of the C++ code for the navfn planner, which is the main planner component of the Navigation Stack. We have ported the planner to a Maude specification, and validated their equivalence using differential testing techniques. For this purpose, we integrated the specification into ROS using a novel high performance Python interface for Maude. We then analyzed the Maude specification by means of model checking and functional verification techniques, using not only the built-in tools of Maude, but also a translation into Dafny, and a manual but systematic generation of verification conditions from the Maude specification. Along the way we also encountered counterexamples for some soundness properties —e.g. that paths should not collide with obstacles— and optimatility —paths should have the lowest possible cost— of the NavFn planner.

Autores: Enrique Martin-Martin / Manuel Montenegro / Adrián Riesco / Juan Rodríguez-Hortalá / Rubén Rubio / 
Palabras Clave: Dafny - Formal Verification - Maude - Model checking - Navigation - Rewriting Logic - ROS

Model-checking strategy-controlled rewriting systems

Strategies are a widespread but ambiguous concept in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware model checker built on top of the Maude specification language, based on rewriting logic, and its strategy language.Pendiente de publicación en «International Conference on Formal Structures for Computation and Deduction» (FSCD) 2019. Se envía la versión aceptada. La versión definitiva estará lista a finales de abril.

Autores: Rubén Rubio / Narciso Marti-Oliet / Isabel Pita / Alberto Verdejo / 
Palabras Clave: Maude - Model checking - Rewriting Logic - strategies

Towards a formal framework for analyzing stream processing systems in Maude (Trabajo en progreso)

With the rise of Big Data technologies, distributed stream processing systems (SPS) have gained popularity in the last years. Among these systems Spark Streaming stands out as a particularly attractive option, with a growing adoption in the industry, so we will consider in particular some features of SPS in Spark Streaming. Maude is a high-performance logical framework where other systems can be easily specified and executed. In this paper we show how a Maude specification of Spark Streaming would allow developers to analyze and prove properties on their programs.

Autores: Adrián Riesco / Miguel Palomino / Narciso Martí-Oliet / 
Palabras Clave: Maude - Model checking - Stream processing systems

Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 (Tutorial)

This paper introduces some novel features of Maude 2.7. We have added support for: (i) built-in order-sorted unification modulo associativity, commutativity, and identity, (ii) built-in variant generation, (iii) built-in order-sorted unification modulo a finite variant theory, and (iv) symbolic reachability modulo a finite variant theory.

Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Martí-Oliet / José Meseguer / Carolyn Talcott / 
Palabras Clave: associativity commutativity and identity - Maude - narrowing - Order-sorted - unification

Partial Evaluation of Order-sorted Equational Programs modulo Axioms (Trabajo de alto nivel)

Partial evaluation (PE) is a powerful and general program optimization
technique with many successful applications. However, it has never been investigated
in the context of expressive rule-based languages like Maude, CafeOBJ,
OBJ, ASF+SDF, and ELAN, which support: rich type structures with sorts, subsorts
and overloading; and equational rewriting modulo axioms such as commutativity,
associativity–commutativity, and associativity–commutativity–identity. In
this paper, we illustrate the key concepts by showing how they apply to partial
evaluation of expressive rule-based programs written in Maude. Our partial evaluation
scheme is based on an automatic unfolding algorithm that computes term
variants and relies on equational least general generalization for ensuring global
termination. We demonstrate the use of the resulting partial evaluator for program
optimization on several examples where it shows significant speed-ups.

Autores: María Alpuente / Angel Cuenca-Ortega / Santiago Escobar / José Meseguer / 
Palabras Clave: Equational Rewriting modulo Axioms - Maude - Partial Evaluation - Rewriting Logic

Prototyping Component-Based Self-Adaptive Systems with Maude

Software adaptation is becoming increasingly important as more and more applications need to dynamically adapt their structure and behavior to cope with changing contexts, available resources and user requirements. Maude is a high-performance reflective language and system, supporting both equational and rewriting logic specification and programming for a wide range of applications. In this paper we describe our experience in using Maude for prototyping component-based self-adaptive systems so that they can be formally simulated and analyzed. In order to illustrate the benefits of using Maude in this context, a case study in the robotics domain is presented.

Autores: Juan F. Inglés-Romero / Cristina Vicente-Chicote / Javier Troya / Antonio Vallecillo / 
Palabras Clave: component-based architecture - Maude - prototyping - Self-Adaptation

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada