Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 The Origins

The story of Maude does not begin on a dark and stormy night as many stories do, but on a sunny Californian day. Maude was conceived at the Logic and Specification Group, part of the Computer Science Laboratory at SRI International, in Menlo Park, California, in the Spring of 1990. José Meseguer was leading that group, after working for several years with J. A. Goguen and other colleagues on order-sorted equational logic [47] and its implementation in the OBJ3 language [48], among many other topics. At that time he was proposing a new computational logic which could provide on the one hand a unified model of concurrency [63, 64], and on the other hand declarative support for (concurrent) object-oriented programming [62, 66]. This new logic was thought of as an extension of (order-sorted) equational logic with rules (understood either as logical inference rules or as transitions in a concurrent system) which, as the equations, would also be executed by rewriting, and for this reason was called rewriting logic. The good properties of the logic for unifying several models of computation, including concurrent ones, were soon generalized to representing other models of computation and also other logics, so that rewriting logic was proposed as a logical and semantic framework [58, 59].

In the same way that order-sorted equational logic was implemented as a specification and programming language in OBJ3, behind rewriting logic there was a language waiting to be implemented. But the language, soon to be called Maude, was there from the beginning. In addition to the papers [62, 66] devoted to the rewriting logic support of object-oriented programming, in those years several other papers were produced from the programming point of view [65, 75, 83], emphasizing the multiparadigm and parallel programming characteristics of the proposal. Moreover, even the more theoretical papers, such as the ones about the logical framework [58, 59], used the Maude notation for presenting examples in such a way that, with slight changes, most of them could be executed in the current implementation of the language. Those examples already used primitive versions of constructs for parameterized specification and some of them were associated with a name, Maudelog, for a version of Maude with logical variables and unification, a feature which has taken much longer to be fully implemented (see Sect. 3). The way “from OBJ to Maude and beyond” has been well explained by José Meseguer himself in [70].

Although the implementation of the Maude language and system were not yet underway, techniques for compilation of rewriting onto parallel architectures were studied as part of the Rewrite Rule Machine (RRM) project [54, 55] in the early nineties. A sublanguage of Maude, called Simple Maude, which included term rewriting, graph rewriting, and object-oriented rewriting, was proposed as part of this project.

The prospects for an implementation of Maude greatly improved in the mid nineties, with the arrival at SRI International of Steven Eker, as a postdoc expert on term rewriting implementation, and Manuel Clavel, as a PhD student to work on rewriting logic reflection [12]. This is indeed the reason for the title of this paper: it is around this date when the Maude team was born. The work developed in that period was shown in the first public presentation of the Maude system [25], which took place at the first Workshop on Rewriting Logic and its Applications (WRLA) in Asilomar, California, in 1996 [67]. Another presentation at the same event showed the first realization of the reflection ideas in rewriting logic and Maude [26].

Coincidentally, Francisco Durán also joined the group during that event, as a PhD student, to work on the Maude module algebra [29], which led to the development of Full Maude. Although the advances of all the work being done by the Maude team in all these areas were shown at the second WRLA in Pont-à-Mousson, France, in 1998 [53] (implementation [17], reflection [13, 15], module algebra [34]), the first public release of Maude had to wait yet another year until the end of 1999 [16]. Maude 1 was presented in RTA 1999 [18], in FASE 2000 [21], in an ETAPS 2000 tutorial [19], and in a journal paper published in 2002 [22].

However, that first public release of Maude was a proof-of-concept. Although it already had many interesting features, there were so many other missing features that it was not the end, but the beginning of much more work, as discussed by the “Towards Maude 2.0” paper [20] presented at the third WRLA in Kanazawa, Japan, in 2000 [45]. It required a lot of effort to complete the implementation and also to write a good manual for Maude 2.0, publicly released in the Summer of 2003, with a presentation in RTA 2003 [23]. Among other new features, this new version provided support for membership equational logic, support for rewrite expressions in rule conditions, new predefined modules, a new version of its metalevel, and an LTL model checker.

The Maude 2 features kept increasing and improving along the following years, when we managed to have yearly releases, helped by intense meetings of the Maude team, at that time distributed in different locations both in the US and in Europe, after each edition of the WRLA, in Pisa (2002), Barcelona (2004), and Vienna (2006). We reached an important milestone with the publication in 2007 of the book “All About Maude” [24]. The book coincided with the release of Maude 2.3, where the main features of the language and its implementation stabilized, including parameterized modules, interaction with external objects, and a greater catalogue of predefined—some of them parameterized—modules and views, among others.

Since then, the Maude team has produced several additional releases until the recent Maude 2.7. Most of the new features in Maude 2.4, presented at RTA 2009 [14], and subsequent versions after it, have been related to order-sorted unification and narrowing, which is the subject of Sect. 3. In this brief summary of the work related to the origins of Maude and rewriting logic we cannot do justice to all the work done by many people around the world in this area; instead, we direct the reader to the survey written by José Meseguer himself on twenty years of rewriting logic, published in 2012 [72], together with an annotated bibliography [60] compiling all the papers on rewriting logic and its applications written in the period 1990–2012.

2 The Language

The close contact with many specification and programming applications has served as a good stimulus for a substantial increase in expressive power of the rewriting logic formalism in general, and of its Maude realization in particular. Maude is a high-performance language and system supporting both equational and rewriting logic computation for a wide range of applications, including development of theorem-proving tools, language prototyping, executable specification and analysis of concurrent and distributed systems, and logical framework applications in which other logics are represented, translated, and executed.

2.1 Generalized Rewrite Theories in Maude

Maude’s functional modules are theories in membership equational logic [9, 69], a Horn logic whose atomic sentences are either equalities \(t = t'\) or membership assertions of the form t : s, stating that a term t has a certain sort s. Such a logic extends OBJ3’s [48] order-sorted equational logic and supports sorts, subsorts, subsort polymorphic overloading of operators, and definition of partial functions with equationally defined domains.

A Maude (system) module is a generalized rewrite theory, defined as a 4-tuple \(\mathcal {R} = (\Sigma ,E\cup Ax,\phi ,R)\), where \((\Sigma ,E\cup Ax)\) is a membership equational theory, Ax is a set of equational axioms for which rewriting modulo is available, R is a set of labeled conditional rewrite rules, and \(\phi \) is a function assigning to each operator \(f : k_1 \ldots k_n \rightarrow k\) in \(\Sigma \) the subset \(\phi (f) \subseteq \{1, \ldots , n\}\) of its frozen arguments. Rewriting in \({(\Sigma ,E\cup Ax,\phi ,R)}\) happens modulo the equational axioms Ax. Maude supports rewriting modulo different combinations of associativity (A), commutativity (C), identity (U), left identity (Ul), right identity (Ur), and idempotence axioms. Computationally, rules are interpreted as local transition rules in a possibly concurrent system. Logically, they are interpreted as inference rules in a logical system. This makes rewriting logic both a general semantic framework to specify concurrent systems and languages [68], and a general logical framework to represent and execute different logics [59]. The combination of evaluation strategies and frozen arguments allows Maude to perform context-sensitive rewriting [57] with both equations E and rules R modulo Ax.

Maude accepts module hierarchies of functional and system modules with user-definable mixfix syntax. The Maude system is implemented in C++ and is highly modular. Maude’s core is its rewrite engine, which is extensible, and indeed has been extended, in many different ways since its inception. For instance, new equational theories can be “plugged in” and new built-in symbols with special rewriting (equation or rule) semantics may be easily added. To date, rewriting modulo all combinations of associativity, commutativity, left and right identity, and idempotence have been implemented apart from those that contain both associativity and idempotence.

Over the years, the development of Maude has been guided by the goal of providing a better support for both rewriting logic and its underlying membership equational logic. For instance, the duality between its logical and operational views was completed with the addition of the nonexec attribute in Maude 2.0. The point is that efficient and complete computation by rewriting is only possible for equational theories that satisfy properties such as confluence, sort-decreasingness, and termination. Similarly, to be efficiently executable, a generalized rewrite theory \(\mathcal {R} = (\Sigma ,E\cup Ax,\phi ,R)\) should first of all have \({(\Sigma ,E\cup Ax)}\) satisfying the above executability requirements, and should furthermore be coherent [36].

Executability is of course what we want for programming; but it is too restrictive for specification, transformation, and reasoning purposes. For this reason, there is a linguistic distinction between modules, that are typically used for programming as executable theories, and theories, which need not be executable and are used for specification purposes, for example, to specify the semantic requirements of actual parameters of parameterized modules, or for theorem-proving purposes. Maude supports specification of arbitrary membership equational logic theories and of arbitrary rewrite theories, while at the same time keeping a sharp distinction between executable and non-executable statements (i.e., equations, memberships, or rules) by means of the nonexec attribute. Fully executable equational and rewrite theories are called admissible, and satisfy the above-mentioned executability requirements. This support for a disciplined coexistence of executable and non-executable statements allows not only a seamless integration of specification and code, but also a seamless integration of Maude with its formal tools.

Maude includes some built-in functional modules providing convenient high-performance functionality within the Maude system. In particular, the built-in modules of integers, natural, rational, and floating-point numbers, quoted identifiers, and strings provide a minimal set of efficient operations for Maude programmers.

2.2 Reflection in Maude

Informally, a reflective logic is a logic in which important aspects of its metatheory can be represented at the object level in a consistent way, so that the object-level representation correctly simulates the relevant meta-theoretic aspects.

Rewriting logic is reflective [12] in the precise sense of having a universal theory U that can represent any finitely presented rewrite theory T (including U itself) and any terms \(t,t'\) in T as terms \(\overline{T}\) and \(\overline{t}, \overline{t'}\) in U, so that we have the following equivalence

$$T \vdash t \rightarrow t' \Longleftrightarrow U \vdash \langle \overline{T}, \overline{t} \rangle \rightarrow \langle \overline{T}, \overline{t'} \rangle .$$

Since U is representable in itself, we can then achieve a “reflective tower” with an arbitrary number of levels of reflection.

Maude efficiently supports this reflective tower through its META-LEVEL module, where Maude terms and modules are reified as elements of a data types Term and Module, respectively. The processes of reducing a term to normal form in a functional module and of rewriting a term in a system module using Maude’s default interpreter are respectively reified by descent functions metaReduce and metaRewrite. Similarly, the process of applying a rule of a system module to a subject term is reified by a function metaApply. Furthermore, parsing and pretty printing of a term in a signature, as well as key sort operations are also reified by corresponding metalevel functions, and up and down functions to move terms, modules, and views between levels.

The reflective capabilities of Maude provide a great range of possibilities, many of which have been exploited with different purposes. It has been used, for example, to define alternative rewriting strategies, to define strategy languages, to define module operations, and in general to extend Maude in different ways. This extensibility by reflection is exploited in Maude’s design and implementation. Full Maude is an extension of Maude written in Maude itself which has been used since the beginnings of Maude as a place in which to design and experiment with new features. For example, a module algebra of parameterized modules, views, and module expressions in the OBJ style was available in Maude through Full Maude [30, 34, 35] long before it was implemented in C++ for (Core) Maude 2.4. Object-oriented modules, with convenient syntax for object-oriented applications, or parameterized views are currently available in Full Maude but not yet in Core Maude. In summary, we have been ‘using our own medicine’, using Maude to specify our system before facing the effort of implementing it. Indeed, Full Maude has been more than a place in which to experiment with new features, it has provided basic infrastructure on which to define extensions of Maude such as Real-Time Maude [76].

The reflective capabilities of Maude have also been key for the development of executable implementations of very different formal models and programming languages. See, e.g., the coordination models for distributed objects in [82] and [73], the definition of Mobile Maude [32] and its socket-based distributed implementation [37], or the Maude Action Tool [28], which provides an executable environment for action semantics.

2.3 Maude’s Formal Tools

In addition to its core functionality for rewriting, Maude comes with a number of tools. Some of these tools are directly integrated in the core system, which provides specific commands for them, as for the search command, for searching for terms satisfying given pattern and condition reachable from a given initial term, or through operators in predefined modules, as in the case of its LTL model checker. Other tools are provided as extensions by different authors, some using the infrastructure provided by Full Maude, such as the Church-Rosser checker, the coherence checker [36], the termination tool [33], the explicit-state model checker for linear temporal logic of rewriting (LTLR) [4, 71], or the LTL logical model checker [2]; and some independently, such as the Maude inductive theorem prover [12], or the sufficient completeness checker [50]. An attempt to bring these tools under a common environment so that they can be used together to keep track of pending proof obligations and help in their interaction to discharge these proof obligations is currently under development in what is being called the Maude Formal Environment [38].

3 The Present: Unification and Narrowing

As mentioned before, Maude inherited many features from its predecessors, such as order-sorted equational logic and the use of commonly occurring attributes like associativity and commutativity, but other features of its predecessors were left behind, e.g., Eqlog [46] envisioned an integration of order-sorted equational logic with Horn logic, providing logical variables, constraint solving, and automated reasoning capabilities on top of order-sorted equational logic; and MaudeLog [65] envisioned an integration of order-sorted rewriting logic with queries including logical variables. The paper [40] revisited this topic and showed how many modern programming features can be implemented using Maude.

Unification is a fundamental deductive mechanism used in many automated deduction tasks and it is essential for programming languages with logical variables. Many functional and logic programming languages use an evaluation mechanism called narrowing [1], which is a generalization of term rewriting allowing free variables in terms (as in logic programming) and replacing pattern matching by unification in order to (non-deterministically) reduce these terms.

Unification and narrowing were introduced in Maude in 2009 as part of the Maude 2.4 release [14]. In that version of Maude, unification worked for any combination of symbols being either free or associative-commutative (AC), and it was developed by Eker as a built-in feature in Core Maude. Narrowing worked for system modules without equations and relied on the built-in unification algorithm. It supported the concept of symbolic reachability analysis of terms with logical variables, computing suitable substitutions for the variables in both the origin and the destination terms. Narrowing was first implemented in Full Maude, which allowed us to carry on research on its reasoning capabilities. The latest developments in Maude 2.6 were presented at RTA 2011 [31]. First, Eker improved the built-in unification algorithms to allow any combination of symbols being either free, commutative (C), associative-commutative (AC), or associative-commutative with an identity symbol (ACU). The performance was dramatically improved, allowing further development of other techniques in Maude. Second, the concepts of variant [27] and variant-based unification [43] led to a significant improvement in the reasoning capabilities. Given an equational theory \((\Sigma , E \cup Ax)\), the E, Ax-variants of a term t are the set of all pairs consisting of a substitution \(\sigma \) and the E, Ax-canonical form of \(t\sigma \). Variant generation, variant-based unification, and symbolic reachability based on variant-based unification were all implemented in Full Maude.

In the most recent Maude 2.7 version, Eker has extended the available capabilities. First, the built-in unification algorithm allows any combination of symbols being free, C, AC, ACU, CU, U, Ul, Ur. Second, variant generation and variant-based unification are implemented in C++ at the Core Maude level with excellent performance. Note that the former version of variant generation and variant-based unification in Maude 2.6 was implemented for very simple equational theories called strongly right irreducible, but the new implementation in Maude 2.7 got rid of this restriction, allowing really complex equational theories and their combinations.

The classical application of narrowing modulo an equational theory is to perform \(E \cup Ax\)-unification by narrowing with oriented equations E modulo axioms Ax. Indeed, the variant-based equational order-sorted unification algorithm implemented in Maude 2.7 is based on a narrowing strategy, called folding variant narrowing [43], that terminates when \(E \cup Ax\) has the finite variant property [27], even though unrestricted narrowing typically does not terminate when Ax contains AC axioms [27, 43].

An interesting example of the flexibility of folding variant narrowing, even beyond equational unification, is given for the classic missionaries and cannibals problem. In this problem, three missionaries and three cannibals must cross a river using a boat. The boat cannot cross the river with no people on board, and cannot carry more than two people. In any of the banks, the missionaries cannot be outnumbered by cannibals, otherwise the cannibals would eat the missionaries.

A solution for this problem was presented by Goguen and Meseguer in [49] as an equational logic program, requiring constraint-solving features, logical variables, order-sorted types, and axioms. Features of the original solution have been adapted to the current equational variant-based programming features available in Maude using the ideas of [40], and the resulting module is shown in Fig. 1.

Fig. 1.
figure 1

Missionaries and cannibals example

Full size image

The imported module TRIPLIST defines trip lists (TripList), with concatenation operator _*_ as constructorFootnote 1 and a length operation #_. Module PSET defines sorts Elem of people and PSet of multisets of people. Multisets are constructed with union operator _+_, which is declared as associative, commutative and with an identity symbol, and come with operators _-_ for removal and

figure a

for intersection.

Our aim is to find a list of trips, where each trip is a term rooted by a predicate boat with a set of missionaries and cannibals. Odd positions in the list represent trips from the left bank to the right bank, and even positions trips from right to left. The MAC module defines constants for the missionaries (taylor, helen, and william) and the cannibals (umugu, nzwave, and amoc). lb(L) (resp., rb(L)) represents the people set in the left (resp., right) bank after the sequence of trips L. mset(PS) (resp., cset(PS)) gives the subset of missionaries (resp., cannibals) in PS. The function boatok checks whether a trip is ok — one or two people in the boat, where these are from the set of defined cannibals and missionaries — and solve is the general predicate for checking/generating the trip list solution — a trip list is a solution if it is a ‘good’ list, and the sequence of trips leaves the left bank empty. A trip list L * T is good if T is a valid trip (boatok), the sublist L is good, and the number of cannibals in each bank is smaller than the number of missionaries in the same bank for each trip in the sequence.

The key is therefore in the definition of the Success sort in the SUCCESS module. The success sort has a constant success, an operator _>>_ that defines the conditional evaluation of constraints, such that the left side is evaluated before the right side, and _=:=_, which represents unification between two terms. For each sort, _=:=_ is defined only in the positive cases, returning success; see below for its definition for sort Bool.

figure b

Folding variant narrowing is performed using those equations labeled with the variant flag, while the remaining equations are used as usual in Maude. Here we can ask for solutions to the very general problem of the names of missionaries and cannibals carried from one side to the other of the river.

figure c

Enumerating all thirty-six solutions takes only a few minutes thanks to the efficient implementation of folding variant narrowing in Core Maude. The most general question is variant unify solve(L) =? success, which enumerates all the necessary boat movements from one bank to the other and the missionaries and cannibals moved each time. However, we would have to add more variant equations, for recursive instantiation of a variable of sort Triplist, and for recursive instantiation of a variable of sort PSet, apart of the current variant equations for instantation of variables of sort Elem. The current implementation in Maude is not able to handle the folding variant narrowing search space associated to a unification problem like that, though it will enumerate the solutions given enough resources.

The modern application of narrowing with rules R modulo \(E \cup Ax\) is that of symbolic reachability analysis [74]. In this case, the rules R are understood as transition rules instead of equations. Narrowing is a complete deductive method [74] for symbolic reachability analysis, that is, for solving existential queries of the form \(\exists \overline{x}\; t(\overline{x}) \rightarrow ^*t'(\overline{x})\) in the sense that the formula holds for R iff there is a narrowing sequence \(t \leadsto ^*_{R,E \cup Ax} u\) such that u and \(t'\) have an \(E \cup Ax\)-unifier. Furthermore, in symbolic reachability analysis, we may be interested in verifying properties more general than existential properties of the form \(\exists X\; t \rightarrow ^{*} t'\), since one can generalize the above reachability property to properties of the form \(\mathcal {R},t \models \varphi \), for \(\varphi \) a temporal logic formula. The papers [2, 42] show how narrowing can be used (again, both at the level of transitions with rules R and at the level of equations E) to perform logical model checking. Two distinctive features are: (i) the term t does not describe a single initial state, but a possibly infinite set of instances of t (i.e., a possibly infinite set of initial states); and (ii) the set of reachable states does not have to be finite. Therefore, standard model-checking techniques may not be usable, because of a possible double infinity: in the number of initial states, and in the number of states reachable for each of those initial states.

So far, the most successful story about rewriting logic with narrowing is the Maude-NPA protocol analyzer [41], where cryptographic protocols are formally specified as order-sorted rewrite theories and the security analysis is performed in a backwards way, from an attack state to an initial state.

4 The Near Future: Rewriting Modulo SMT

The rapid progress of satisfiability modulo theories (SMT) solvers [7] has been one of the most important developments in automated verification and reasoning. A feature recently added to Maude (in an internal version, not publicly released at the time of the publication of this paper) is support for rewriting modulo SMT [78], so that functional and system modules can have conditions dealing with SMT data types, which are then solved by the usually more effective SMT solvers.

SMT solvers are decision procedures for an existential fragment of first-order logic with equality, where variables range over SMT data types, such as Booleans, integers, and reals. After presenting the way in which rewriting modulo SMT is being implemented in Maude in Sect. 4.1, we describe a sample application in Sect. 4.2.

4.1 Maude SMT

When performing rewriting modulo SMT, the object being rewritten is a symbolic representation of a (possibly infinite) family of terms. In its current Maude implementation, the representation of such family of terms is an ordered pair, where the first component is a term which may include variables ranging over data types supported by an SMT solver and SMT operators on those variables, and the second component is a constraint on those SMT variables. Rewriting proceeds as a search where each rewrite rule may have a condition, interpreted as an SMT constraint. In order to make a rewrite step, the accumulated constraints must be satisfiable, as checked by an SMT solver; when a conditional rule succeeds, the constraint it enforced on the SMT variables in the new term is ‘conjuncted’ with the existing constraint. Since Maude has no built-in knowledge of the SMT theories, no simplification of the accumulated constraint is performed.

Maude’s interface to SMT data types closely follows the SMT-LIB standard [6]. In particular there are functional modules BOOLEAN, INTEGER, REAL, and REAL-INTEGER which provide signatures for the SMT-LIB theories of Booleans, integers, reals, and reals combined with integers, respectively. Although the current implementation has some restrictions, we expect to have a full implementation of rewriting modulo SMT in a near future release of Maude.

An SMT rewriting search is initiated with the smt-search command, which has a syntax similar to the syntax of the search command. The start term may only include SMT variables, which may also appear in the pattern term, and condition.

To give a flavor of how rewriting modulo SMT works, let us consider a small example. We define the \({ gcd}\) function using state transitions on a pair of SMT integers that encode Euclid’s algorithm.

figure d

We then ask about the existence of a pair of integers X, Y such that \({ gcd}(X, Y) = 3\) and \(X + Y = 27\).

figure e

Maude searches the (typically infinite) tree of SMT rewrites on (term, constraint) pairs for a state that matches the pattern and satisfies the constraint on the variables given in the command. In the success case, it returns a substitution for non-SMT variables in the pattern and a satisfiable constraint on SMT variables. If the search graph is infinite as in this case, the command will not terminate in the failure case unless a depth bound is given.

Like most other Maude commands, smt-search is reflected at the metalevel by a corresponding descent function.

Currently, Maude uses CVC4 [5] as its backend SMT solver, however calls to the SMT solver are implemented via an abstract interface and wrappers for other SMT libraries could easily be added in the future.

4.2 Symbolic Analysis of Distance-Bounding Protocols

Having the possibility of using constrained variables gives us the opportunity of making finite potentially infinite search spaces. As for a more interesting application of rewriting modulo SMT, let us consider the case of distance-bounding protocols [10], a class of security protocols that infer an upper bound on the distance between two agents from the round trip time of messages. This is used, for example, for controlling some kinds of access and for clock synchronization. In a distance-bounding protocol session, the verifier (V) and the prover (P) exchange messages:

$$ \begin{array}{l} V \rightarrow P : m \\ P \rightarrow V : m' \end{array} $$

where m is a challenge and \(m'\) is a response message (constructed using the components of m such as nonces in m). In order to infer the distance to the prover, the verifier remembers the time, \(t_0\), when the message m was sent, and the time, \(t_1\), when the message \(m'\) returns. From the difference \(t_1 - t_0\) and the assumptions on the speed of the transmission medium, v, the verifier can compute an upper bound on the distance to the prover, namely \((t_1 - t_0) \times v\).

In [52], a novel attack on distance bounding called attack in-between-ticks is presented. The attack is formalized using a model in which provers, verifiers, and attackers may have different clock rates, processing speeds, or observation granularity. The model is based on a multiset-rewriting formalism called timed local state transition systems [51] which supports both discrete and dense time. The key insight for the attack is that an attacker can mask his location by exploiting the fact that a message may be sent at any point between two clock ticks of the verifier’s clock, while the verifier measures the time at discrete clock ticks. For example, if the time bound is 3, a message could start at time 1.7, which is 2 on the verifier’s clock, and the reply received at 4.9, which is 5 on the verifier’s clock. From the verifier’s perspective the attacker is within range, since \(5 - 2 = 3\), but in fact the round trip time was \(4.9 - 1.7 = 3.2\).

The model was formalized in Maude SMT and smt-search was used to find a symbolic representation of a family of attacks. Using Maude SMT the potentially infinite search space becomes finite, by treating the distance between the verifier and the prover as a constrained variable.

To illustrate the use of SMT, we show the Tick rule which advances system time following the approach of Real-Time Maude [76].

figure f

Here, a system state is a soup of timed facts (F @ T) enclosed in brackets. There is a unique fact, Time @ T, representing the physical time. The fact vTime @ T1 represents time as perceived by the verifier. In Real-Time Maude execution and search use a time sampling strategy. In contrast, using Maude SMT the new time is left symbolic, with constraints on its range. Here the constraint says that the next time should be greater than the current time, but should not advance beyond the next verifier time (\(T1 + 1\)).

The following command searches for a state in which the verifier, v, accepts a reply from the prover, p, (Ok(< p, M:Msg>) @ T:Real), where the distance bound is 3 (the allowed round trip time is 2 * 3) and the distance from the verifier to the prover, dvp, (or to an attacker, dva) is greater than 3.

figure g

One (simplified) solution is:

figure h

The verifier’s start time is 1/1 thus the elapsed time is toInteger(dvp + dvp)<= 2/1 * 3/1.

5 Pathway Logic

There have been many applications of Maude in many different areas, including some as diverse as security [41], cyber-physical systems [3, 44], and model-driven engineering [8, 77] (see, for example, the survey [72]). We very briefly discuss in this section one of them, Pathway Logic, which innovates by modeling nature rather that the usual digital artifacts, very nicely illustrating the modeling capabilities of Maude.

Pathway Logic (PL) is a system for modeling and reasoning about cellular processes such as signal transduction, metabolism, and cell-cell communication in the immune system. The semantic underpinnings of PL is Maude, and José Meseguer was part of the original PL team that developed the key ideas [39]. The first instance of a PL model was a model of a cancer-related signaling pathway crafted in Maude in 2000. In order to facilitate scaling up and interacting with the PL models, the executable Maude model has been augmented with the Pathway Logic Assistant (PLA), an interactive graphical interface that allows a user to easily create specific models, and browse and query them [81]. In addition, a mechanism for semantically grounding the language with links to standard databases has been put in place, and a substantial collection of formal models has been developed [56, 80].

5.1 About Pathway Logic

Signal transduction is the mechanism by which cells sense their environment, process this information, and make decisions: what proteins to produce, what metabolic pathways to activate, whether to replicate, move, or possibly die. Typically, the signal is a chemical or protein in the cells environment that binds to a receptor protein (in the cell membrane). The receptor becomes active, initiating the signaling process. The signal is transmitted by change in state and location of proteins involved.

In PL a cell state is represented as a soup of occurrences, where each occurrence has three components: a protein or other biomolecule (gene, metabolite, etc.), a modifier, and a location. The modifier indicates the state of the protein, including binding of small molecules or phosphates, or ability to act on other proteins (enzyme activity). For example, the term < [Hras - GTP], CLi> is the occurrence of the protein Hras modified by binding to the small molecule GTP (Guanosine TriPhosphate), attached to the inside of the cell membrane (CLi). Footnote 2 Signal transduction steps are formalized as local rewrite rules operating on the relevant part of the cell state.

As an example, rule 1.EgfR.act formalizes the initiation of signaling in response to the presence of Egf (Epidermal growth factor) in a cell’s exterior.

figure i

Here, ?ErbB1L:ErbB1L is a variable of sort ErbB1L, XOut is the cells external environment, and the infix operator _:_ represents complex formation. In the model there are two proteins of sort ErbB1L: Egf and Tgfa (Transforming growth factor alpha).

Fig. 2.
figure 2

Activation of Hras in response to Egf. The full subnet with two execution paths compared. Pink belongs to both paths, blue and cyan to different paths. Ovals represent occurrences, rectangles represent rules, with input ovals connected by incoming arrows and output connected by outgoing arrows. Dashed arrows connect occurrences that both input and output (enzymes) (Color figure online).

Full size image

How does the Egf signal propagate? To answer the question, we use the PLA. Figure 2 shows the subnet containing all rules relevant to activation (binding to GTP) of Hras in response to Egf. The subnet is generated by backwards collection from the goal H =< [Hras - GTP], CLi> in the Egf response network.

A specific execution path can be found by mapping the subnet and goal to the language of the LoLA model checker [79] asserting that the goal cannot be reached. If there is a counter example, LoLA returns a list of transitions that can be fired to reach the goal. Maude then converts this to a network and generates the expression to display the interactive graph.

Figure 2 also shows the result of comparing two different execution paths, the second is the result of removing one of the occurrences from the subnet (simulating a knockout) before asking LoLA.

5.2 Maude’s Role in Pathway Logic

The integration of the Maude executable model and PLA is achieved using the IOP platform for communication amongst a group of actors. Maude’s loop mode and reflection are key to turning Maude into an actor [61]. The PL Maude actor extends the IMaude actor [61] with rules for handling PL specific requests. IMaude provides data structures for representing state, managing asynchronous interaction, and saving and restoring state. The latter makes essential use of Maude’s capabilities for pretty-printing and parsing. PLA is an actor built using an interpreter of a Scheme-like language, JLambda, layered on top of Java. The Maude PL actor listens for requests from PLA and generates expressions in the JLambda language to instruct PLA to construct and render interactive network graphs.

Proteins, modifications, and locations are given different names by different biologists. Thus, to understand what a biological model is talking about it is important to link the names (constants) used to reference databases that provide canonical names and additional information. This is accomplished using the metadata attribute of Maude operator declarations. PL operator metadata is a string encoding an S-expression that maps key words to values such as database access identifiers, synonym lists, and biological classifiers. With the aid of a metamodel (componentInfoSpec) the metadata is rendered as a menu of information and active links that are presented when the user clicks on a graph element. The following is the operator declaration for Egf. The metadata includes identifiers used by two reference databases (spnumber for UniProt and hugosym for HGNC), as well as a list of synonyms that can be used when a user unfamiliar with PL naming is searching for information.

figure j

Another important requirement for a model is to justify the rules describing signal transduction steps. Where do these rules come from? They are inferred from experimental observations of what is present in a cell (and where) and of response of a cell or a population of cells to different perturbations. In PL each rule is linked (via metadata) to an evidence page that contains a formal representation of the experimental observations used in inferring the rule. Footnote 3

As noted above, the PL rule base consists of symbolic rules that have variables whose sort consists of a finite set of proteins or modifications or locations. Petri net tools (and graphical representations) need concrete instances. One possibility is simply to generate all possible instances. This generates many useless rules, because proteins of a given sort behave similarly in some cases, and differently in other cases. Thus we take advantage of the Maude function to generate all matches of a rule to a given state to generate only concrete rules that are possibly reachable from initial states of interest.

In the spirit of May I borrow your logic [11], PL supports multiple representations of a PL knowledge base: Maude signature and rules, Petri nets, JSON, and SBML (Systems Biology Markup Language). The Petri net representation is used for efficient analysis of large networks that takes advantage of the restricted nature of PL rules. SBML is an exchange format used to share models between different systems biology tools including simulators and visualizers. The JSON representation is used to treat a PL knowledge base as a database with efficient query of static relations; for example, finding all rules that involve the protein whose UniProt identifier is P01112 (Hras). Maude could be programmed to answer such queries, but putting the information in a database makes it more widely accessible. In addition, the JSON representation is an easily parsable exchange format that is being used by researchers developing modeling and analysis tools.

Transformations to different representation systems is done by reflecting the PL model to the metalevel and transforming it to a representation in the target system, which can then be written to a file with the help of the PLA actor.

6 Further Ahead

We have presented our view of the two decades we have been involved in the development of Maude. We have gone from the first years of Maude to the current state of the system and the new features currently under development. What features will Maude users be expecting in the future? Or what features will have a bigger impact for Maude in the future? As we explained before, a current trend in programming languages is to become multi-paradigm, offering flexibility and simplicity for problem specification and solving, and we believe our efforts will go into that direction.

On the one hand, all the logical and symbolic features will be boosted. For instance, other SMT libraries such as veriT could be added to Maude. Also, variant generation and variant-based unification, as well as narrowing in system theories, consider only unconditional rules and equations: conditional narrowing, both at the level of equational logic and rewriting logic, should be added. Moreover, more built-in unification algorithms will be included in Core Maude: we have explored unification algorithms for associativity, for homomorphic encryption, for exclusive-or, etc. Furthermore, we envision conditional narrowing combined with SMT solvers, so that many different reasoning facilities are seamlessly combined.

On the other hand, tool support will be incremented. Maude would not be such a good logical framework without its metalevel capabilities. The Maude Formal Environment will be improved with better tool integration. And we should not forget about tools built on top of Maude, such as the Pathway Logic Assistant, Real-Time Maude, or the Maude-NPA protocol analyzer.