Statistical Model Checking of eMotions DomainSpecific Modeling Languages
 3 Citations
 687 Downloads
Abstract
Domain experts may use novel tools that allow them to design and model their systems in a notation very close to the domain problem. However, the use of tools for the statistical analysis of stochastic systems requires software engineers to carefully specify such systems in low level and specific languages. In this work we line up both scenarios, specific domain modeling and statistical analysis. Specifically, we have extended the eMotions system, a framework to develop realtime domainspecific languages where the behavior is specified in a natural way by inplace transformation rules, to support the statistical analysis of systems defined using it. We discuss how restricted eMotions systems are used to produce Maude corresponding specifications, using a model transformation from eMotions to Maude, which comply with the restrictions of the VeStA tool, and which can therefore be used to perform statistical analysis on the stochastic systems thus generated. We illustrate our approach with a very simple messaging distributed system.
Keywords
Model Check Model Transformation Operational Semantic Concrete Syntax Statistical Model Check1 Introduction
Model Driven Engineering advocates the use of models as the key artifacts in all phases of development, artifacts from which whole systems can be derived, analysed and implemented [21]. To be able to define such models in terms as close to the problem domain as possible, different technologies for the definition of Domain Specific Modeling Languages (DSMLs) have been proposed (see, e.g., [20]). The main goal of these DSMLs is to follow the domain abstractions and semantics, allowing modelers to perceive themselves as working directly with domain concepts. Model transformations may then be used to analyze certain aspects of models and then automatically synthesize various types of artifacts, such as source code, simulation inputs, or alternative model representations.
DSMLs are typically defined by means of its structural aspects (with its corresponding abstract and, in some cases, concrete syntaxes). These definitions allow the rapid development of languages and some of their associated tools, such as editors or browsers. Typically, to perform some type of analysis or to generate code, such models need to be transformed into formalisms or programming languages with the appropriate tool support. There are many success stories using this approach. However, the semantics of such DSMLs is embedded in the model transformations, and provided by the target formalism, what constrains the rapid definition of such languages. To overcome this situation different authors have proposed different ways of providing an operational semantics as part of the definition of DSMLs, possibly being the most successful one the one using graph transformation systems (GTS) [33], with systems such as AToM3 [13], AGG [37] or eMotions [29] implementing it.
The specification of the explicit behavioral semantics of DSMLs helps in MDE activities such as quick prototyping, simulation, or analysis. Ensuring semantic properties of models is important because any error in a model can easily become a systemic error in the system under development. E.g., AGG and eMotions provide support for the simulation of models defined conforming to userdefined DSMLs. These and other languages provide support for different kinds of analysis as well, like termination checks, critical pair analysis, or reachability analysis (see, e.g., [31, 37]). CheckVML [34], GROOVE [28] and eMotions [29] support the model checking of systems whose behavior is specified by graph transformation systems.
This is, however, not enough, since applications become more and more complex, and model checking is a very expensive procedure, both in time and space, being infeasible in many cases. A very important class of systems that falls out of the scope of classical model checkers are realtime stochastic systems. The methods used to verify quantitative properties of stochastic systems are typically based on numerical methods [19], that iteratively compute the exact (or approximate) measure of paths satisfying relevant logical formulas. Although tools like PRISM [22] and UPPAAL [4] have shown very successful in the analysis of this kind of systems, explicitly constructing the corresponding probabilistic model is infeasible in many cases. An alternative method that solves this problem is based on statistical methods, similar to Monte Carlo simulations. By testing our hypothesis on many executions of a system, we may infer statistical evidence on the satisfaction or violation of the specification. Thus, properties like “the probability of completing task X with Y units of energy is greater than 0.3” or “the average amount of energy required to complete task X with confidence interval \(\alpha \) and error bound \(\beta \)” are evaluable. YMER [39] and VeStA [36] were pioneering tools implementing these techniques. Latest releases of the wellestablished tools PRISM and UPPAAL have more recently also included capabilities for statistical model checking (see [9, 23]).
Statistical methods has another advantage in the context of DSMLs: are “easy” to use and “cheap”. As other modelchecking methods, statistical model checking is completely automatic, and can be used where other methods fail. But can also be used for “normal” systems with a shorter computation time. Since statistical model checking assumes the existence of inaccuracy in its results, answers are calculated provided a confidence interval and an error bound. As may be expected, these requirements have an impact on the number of samples to be processed, and therefore on the evaluation time.
In this paper we describe how the eMotions tool has been extended so the models built conforming to userdefined DSMLs are suitable for statistical model checking. eMotions models are transformed into Maude specifications satisfying the requirements of the PVeStA tool [3] (an extension and parallelization of VeStA [36]). Such Maude specifications are therefore suitable to be stochastically analyzed using PVeStA. We illustrate the use of eMotions to model systems and its statistical model checker with a very simple messaging system.
The remaining of the paper is structured as follows. Section 2 presents eMotions and VeStA/PVeStA, and their underlying Maude system. Section 3 explains how eMotions specifications are statistically analysed using PVeStA and how the connection between these two systems is established. The way systems are defined in eMotions and how they can be statistically analysed is illustrated with a case study in Sect. 4. Section 5 discusses some related work and Sect. 6 wraps up presenting some conclusions and future work.
2 Preliminaries
In this section, we introduce the eMotions language and tool, the Maude system and the Maude implementation of eMotions, and the VeStA/PVeStA tool.
2.1 The eMotions System
eMotions [29] is a graphical language and framework that supports the specification, simulation, and formal analysis of realtime systems. It supports the graphical specification of the dynamic behavior of DSMLs using their concrete syntax, making this task very intuitive.^{1} The abstract syntax of a DSML is specified as an Ecore metamodel, which defines all relevant concepts—and their relations—in the language. Its concrete syntax is given by a GCS (Graphical Concrete Syntax) model, which attaches an image to each language concept. Then, its behavior is specified with (graphical) inplace model transformations. eMotions provides a model of time, supporting features like duration, periodicity, etc., and mechanisms to state action properties [29, 30].
Inplace transformations are defined by rules, each of which represents a possible action of the system. These rules are of the form \([\text {NAC}]^{*}\times \text {LHS}\rightarrow \text {RHS}\), where LHS (lefthand side), RHS (righthand side) and NAC (negative application conditions) are model patterns that represent certain (sub)states of the system. The LHS and NAC patterns express the conditions for the rule to be applied, whereas the RHS represents the effect of the corresponding action. A LHS may also have positive conditions, which are expressed, as any expression in the RHS, using OCL. Thus, a rule can be applied, i.e., triggered, if a match of the LHS is found in the model, its conditions are satisfied, and none of its NAC patterns occur. If several matches are found, one of them is nondeterministically chosen and applied, giving place to a new model where the matching objects are substituted by the appropriate instantiation of its RHS pattern. The transformation of the model proceeds by applying the rules on submodels of it in a nondeterministic order, until no further transformation rule is applicable.
In eMotions, there are two types of rules to specify timedependent behavior, namely, atomic and ongoing rules. Atomic rules represent atomic actions with a duration, which is specified by an interval of time. Atomic rules with duration zero are called instantaneous rules. On the other hand, ongoing rules represent continuous actions that may be interrupted at any time.
A special kind of object, named Clock, represents the current global time elapse. Designers can use it in their rules (using its attribute time) to know the amount of time that the system has been working.
2.2 Maude
Maude [10, 11] is an executable formal specification language based on rewriting logic [24], a logic of change that can naturally deal with states and nondeterministic concurrent computations. A rewrite logic theory is a tuple \((\varSigma ,E,R)\), where \((\varSigma ,E)\) is an equational theory that specifies the system states as elements of the initial algebra \(\mathcal {T}_{(\varSigma ,E)}\), and R is a set of rewrite rules that describe the onestep possible concurrent transitions in the system.
Rewriting will operate on congruence classes of terms modulo E. This of course does not mean that an implementation of rewriting logic must have an Ematching algorithm for each equational theory E that a user might specify. The equations are divided into a set A of structural axioms for which matching algorithms are available and a set E of equations. Then, for having a complete agreement between the specification’s initial algebra and its operational semantics by rewriting, a rewrite theory \((\varSigma ,E\cup A,R)\) is assumed to be such that the set E of equations is (ground) ChurchRosser and terminating modulo A, and the rules R are (ground) coherent with the equations E modulo A (see [14, 15]).
In the case of Maude, the equational logic is membership equational logic (MEL) [7], which can be seen as an extension of ordersorted logic with sorts, subsorts, and partial functions, and where atomic sentences include both equations \(t=t'\) and memberships t : s, stating that term t has sort s. Maude provides support for rewriting modulo associativity, commutativity and identity, which perfectly captures the evolution of models made up of objects linked by references as in graph grammar.
Maude counts with a rich set of validation and verification tools, increasingly used as support to the development of UML, MDA, and OCL tools (see, e.g., [32] for an overview). Furthermore, Maude has demonstrated to be a good environment for rapid prototyping, and also for application development (see [11]).
2.3 Maude Representation of eMotions Models and Metamodels
As in [5, 32], the algebraic semantics of an Ecore^{2} metamodel \(\textit{MM}\) is provided by a MEL theory \( Spec _{ MM }\) so that a model M conformant with \( MM \) is an element of the initial algebra \(\mathcal {T}_{ Spec _{ MM }}\). The eMotions definition of a domain specific language provided by a metamodel \( MM \) plus a set of transformation rules defining its dynamic semantics, is then represented as a rewrite theory extending \( Spec _{ MM }\) with some additional definitions and rules specifying such a behavior.
An ATL transformation transforms eMotions models into Maude executable specifications, which can be used for simulation and analysis. Although a detailed presentation of this transformation can be found in [30], we give here a general account of it to understand the rest of the paper.
eMotions’ models are represented in Maude as structures of sort @Model of the form \(mm \{ obj_1 \; obj_2 \; ... \; obj_N \}\), where mm is the name of its metamodel and \(obj_i\) are the objects that constitute the model. An object is a recordlike structure of the form \(< o : c\ \ a_1 : v_1 \# ... \# a_n : v_n >\) (of sort @Object), where o is the object identifier (of sort Oid), c is the class the object belongs to (of sort @Class), and \(a_i : v_i\) are attributevalue pairs (of sort @StructuralFeatureInstance). Given appropriate definitions for all classes, attributes and references in its corresponding metamodel, a possible valid state could be as follows:
This code snippet shows part of a model in which there is a node object "n1" of class Node which is connected to channels "ch1" and "ch2", which in turn are connected to nodes "n2" and "n3".^{3}
Although in eMotions there are two kinds of rules, namely, atomic and ongoing rules, for the purpose of the work at hand only atomic rules are used. So in what follows, we sketch the Maude specification of the atomic eMotions rules.
As above explained, time elapse is modeled by using the delta and mte functions. Both functions need to be defined only over timedependent elements, namely the Clock instance and AAE objects. The delta function decreases AAE timers and increases the clock value. The rest of objects remain unchanged.
Action execution objects AAE gather additional information for dealing with scheduling, periodicity, etc. The interested reader is referred to [30] for a complete account on them and on the representation of ongoing rules. From the point of view of executability by rewriting and, in particular, for the discussion on unquantified nondeterminism in the following sections the key idea is that AAE objects are required for the realization of actions.
2.4 The VeStA/PVeStA Tool
There are two main approaches for statistical model checking: sequential testing [40], implemented, e.g., in Ymer [39], and blackbox testing [35], implemented, e.g., in VeStA [36]. In sequential testing, sample execution paths are generated until its answer can be guaranteed to be correct within the required error bounds. In blackbox testing, the system is not controlled to generate specific execution traces. Instead, a quantitative measure of confidence is computed for given samples.
VeStA [36] performs discreteevent simulation from a Maude specification by invoking the Maude interpreter. Given a Maude model, an initial state (or configuration) and a temporal logical formula expressed in QuaTeX [2], VeStA is used to perform stochastic analysis. QuaTeX uses realvalued states and path functions to quantitatively specify properties about probabilistic models. Specifically, QuaTeX provides an expressive language for realvalued temporal properties through the combination of recursive function declarations, an ifthenelse construct, and a next operator. The reader is referred to [2] for a detailed account on QuaTeX. For the soundness of the analysis carried out in VeStA, the specification to be analyzed has to have absence of unquantified nondeterminism [35].
AlTurki et al. have extended the VeStA tool with a parallel implementation, PVeStA [3], which makes the analysis substantially more efficiently. VeStA and PVeStA have been used for the analysis of systems and algorithms by different authors (see, e.g., [1, 8, 16]).
3 PVeStACompliant Representation of eMotions Models
When rewriting a system, there might be different sources of nondeterminism. Some of them are part of our specification, due to probabilistic choices and stochastic realtime. However, rewrite engines need to take their own choices. When there are several matches, for a given rule or for several rules, rewrite engines will choose an alternative following some internal criteria. For the statistical analysis used in VeStA/PVeStA to be sound the rewriting logic specification cannot contain unquantified nondeterminism [2].
The thus obtained specification may be used for rewriting in Maude, but other tools in the Maude formal environment, as its model checker or its reachability analysis tool, can also be used on it [31]. In Sect. 3.2 we show how, by meeting its requirements, we can also use the PVeStA tool for carrying on statistical model checking.
3.1 Unquantifiednondeterminismfree eMotions Systems
Writing an arbitrary rewrite specification that meets the unquantifiednondeterminism free requirement is nontrivial. We could check whether a specification meets the requirement by performing a critical pair analysis and checking that there are no rules that can be applied simultaneously.^{4} However, the checking would not be easy either. And although it may give us some hints on the sources of unquantified nondeterminism, we would still have to change the specification.
To avoid this problem, and to make easier to write a specification free from unquantified nondeterminism, Agha et al. propose in [2] the use of the actor model. To guarantee that only one rule can be fired at any time, messages are scheduled following a continuous probability distribution. To improve its executability, a centralized scheduler is used in [3], so that only one scheduled message or object is available for execution at any time. With this schedulerbased scheme, having a single message in the initial configuration, rules with one object and a message in its lefthand sides, and no two rules for the same message, are a sufficient condition to meet the requirement. Eckhardt et al. relaxed the requirements on systems in [16] by allowing nested configurations of objects. The basic idea is however the same one, if every rule is going to be fired by a message, this message determines the rule match, and there is only one message out of the scheduler at a time, there is only one rule that may be fired and in one possible way.

There is a distinguish class Message whose objects represent messages.

Objects communicate through asynchronous message passing, avoiding direct synchronization among them. We allow several objects in the lefthand sides of rules, but only when they are related by a containment relation, and not to model communication between them.

Message and action execution objects are scheduled so that there is only one of these objects out of the scheduler.

In the initial configuration there is only one message object, and no action execution object. If there are more than one message objects, they have to be scheduled.

Rules may be fired either by messages or by action execution objects AAE. Each rule has in its lefthand side either a message or an action execution object. There is no rule without one of these objects in its lefthand side.

As in [3], there might be in the righthand side of a rule any number of message and action execution objects, but only one may be nonscheduled. The rest must be scheduled so that only one remains in the underexecution configuration. When there are several messages in the lefthand side of a rule, the order of the messages is specified in the transformation.

If there are two rules with the same message or action execution object in its LHS, they cannot be simultaneously applicable. This is a requirement often used in critical pair analysis (cf. [15]): if there is a critical pair between two rules, their conditions should not be simultaneously satisfiable.

The duration intervals of all atomic rules must be of the form [n,n]. Intervals of the form [n,m] are a source of unquantified nodeterminism, since the actual duration of the corresponding action might be any value in that interval.
These requirements are a sufficient condition for the specification to meet the unquantifiednondeterminismfree condition. Given the direct transformation between eMotions rules and Maude rules, these requirements can indeed be checked on the eMotions model itself.
Our scheduler contains both messages and action execution objects, which are released one by one in every rewriting tick step. As in [3], the elements in the scheduler are ordered according to their scheduled time. Messages are always ahead of actions, as they are ready to be consumed as soon as they are generated by a realization rule. Those objects scheduled for the same time are served in accordance with the time they were inserted in the scheduler (FIFO). The order of AAE objects is determined by their timers, being the first action execution object the one with the smallest timer. If several action execution objects have the same countdown, they follow a FIFO order.
 1.
there is a message which matches the message of the lefthand side of an instantaneous rule or a triggering rule of a noninstantaneous rule, or
 2.
there is an AAE object whose countdown has reached zero.
Let us check these requirements on the example given in Sect. 2. The first observation is that there is a single message (Mail or Token) in the lefthand side of each rule. If we assume that the initial configuration has a single message (a Token object in our case), the scheduler will make sure that there is only one message at a time in the running configuration. Notice that NewMessage is the only rule that have two messages in its righthand side. In this case, the transformation generating the Maude specification will decide which one goes first in the scheduler. The other important observation is that there will never be two nodes referencing to the same Mail object. In those other cases in which there are possible overlaps, indicating that there may be more than one applicable rule, or multiple matches for the same rule, we can check that their conditions are not simultaneously satisfiable. See for example that with a Token object in the running configuration, there might be matches for rules NewMessage and DecreaseToken at the same time. Notice however that NewMessage requires e.t = 0 and DecreaseToken requires e.t > 0. There is a similar situation for rules Node2Channel and MessageArrival, in this case Open image in new window and m.to = n.id cannot be satisfied simultaneously.
3.2 Modifications of Maude Rules
The Maude modules supporting the eMotions infrastructure and the Maude rules mapped from the eMotions rules have been modified to make use of the scheduler. Regarding the infrastructure modules, a new module defines the scheduler, operations to insert and remove objects from the scheduler, and extensions to the operations delta and mte. This module is independent from the systems and is added to the resulting Maude specification.
Every Maude rule mapped from an eMotions atomic instantaneous rule must be modified by wrapping all the messages in its righthand side with the operator schedule, which takes a list of one or more elements and insert them in the scheduler, following equations defined in the infrastructure module. For the Maude rules mapped from eMotions noninstantaneous rules, there are more modifications. Messages present in the lefthand side of the triggering rule cannot be removed when the rule is executed, they must be available in the system because they are required for the corresponding realization action. However, they cannot stay free in the configuration because they could be chosen again. Therefore, they must be wrapped with the operator blocked, allowing to free another scheduled message from the scheduler. AAE objects created on the RHSs of rules have to be included within schedule operators to be handled by the scheduler. For the realization rules, messages that appear on its LHS must be wrapped with blocked operators, since the have to match with those wrapped in the triggering rule. Finally, those messages created in such rules have to be enclosed within schedule operators. The eMotions scheduler releases a new message or AAE object if the current state of the system has no free message or AAE after a rewriting step.
In eMotions systems time advances by means of the tick rule which, given the current state, computes the minimum among the maximum time elapses (MTEs) of the actions that may be performed on the current state. If that value is greater than zero, it means that there is no action that can be triggered or realized at that time. In that case, the global time is advanced until that value and the countdown values of all the AAE objects are updated according to that value. The operation delta makes that update. The operations delta and mte have been modified to take into account the elements contained in the scheduler.
3.3 eSMC: eMotions & PVeStA Integration
A new extension for the eMotions framework has been developed to allow automatic modifications of eMotions specifications for them to hold the restrictions mentioned in Sect. 3.2. This extension is named eSMC and it has been implemented as an Eclipse plugin, integrated with the eMotions tool. eSMC encapsulates all the process from the mapping from the eMotions system to the Maude specification to the execution of PVeStA as statistical analyzer, and the presentation of the analysis results. eSMC also allows the user to specify the QuaTeX query that describes the property to be analyzed. The eSMC tool, its documentation and some examples are available at http://maude.lcc.uma.es/esmc.
In the eMotions framework, the model described with the DSML passes through a series of transformations to finally generate a Maude specification. The first one is an ATL modeltomodel transformation, which generates Maude models conforming the Maude metamodel. The second one is a Xtend transformation which generates the final Maude code. eSMC includes a new modeltomodel transformation from the generated Maude models by the ATL transformation to Maude models compliant with the PVeStA restrictions. This new Maude models are, in turn, passed as input to the Xtend transformation.
4 Case Study: A Simple Messaging System
We illustrate the kind of statistical model checking we may perform with the very simple messaging system introduced in Sect. 2. To better illustrate the possible kinds of analysis, we compare the first simple messaging protocol results with a second version of the system in which each node has a routing table to decide which channel the message will be sent through in rules NewMessage and Channel2Node. In this second version, instead of probabilistically choosing an output channel, the value of the via attribute is retrieved from a table storing the best channel for a given destination.
The most interesting property to be analyzed in these simple message passing systems is how well connected is each node? Or how long does it take a message to reach its target? However, this property has to be statistically analyzed, since it depends on the value of three stochastic parameters: (i) when is the next message going to be sent, (ii) which is the target node, and (iii) which channel chooses a node to send the message through. In terms of statistical modelchecking, the property at hand could be expressed as “with a confidence of 99 %, which is the mean time a message takes to commute between the source and target nodes?”.
We proceed by defining a state expression which retrieves the mean response time collected by the Observer object at that time. Our executions have been performed using 8 threads (servers in the PVeStA terminology) and a master (client in PVeStA terms) running batches of 30 samples on each thread. After several iterations PVeStA returns the mean time elapsed between the start node \(n_i\) sending the message and the target node receiving it.
For the case of simple message passing with routing tables the time elapsed for messages sent from each node has been drastically reduced. Note that in the first case there may be even messages looping without finding their target. In this case we run batches of 10 samples on each thread, since it takes a smaller amount of values to converge.
Execution times and mean time for messages being sent
Simple message passing  Simple message passing routing  

\(n_i\)  Ex. time  # samples  \(mean.\ time\)  Ex. time  # samples  \(mean.\ time\) 
\(n_1\)  \(93\,s\)  600  8.7795  \(23\,s\)  240  2.9484 
\(n_2\)  \(111\,s\)  660  7.2204  \(18\,s\)  160  2.9639 
\(n_3\)  \(96\,s\)  870  7.6253  \(16\,s\)  160  2.9984 
\(n_4\)  \(92\,s\)  510  8.3019  \(18\,s\)  160  3.0141 
\(n_5\)  \(87\,s\)  1080  7.7106  \(25\,s\)  240  3.0233 
5 Related Work
Heckel et al. propose in [17] the modeling and analysis of stochastic graphs transformation systems by defining Continuous Time Markov chains from GTSs with transition matrices representing the probabilities of the application of each rule. They provide some support using GROOVE [28] and PRISM. In later works [38], they handle distributions depending on pairs rulematch and may perform stocastic simulation. They develop GRaSS, with VIATRA as backend, which can run multiples simulations limited by a time amount or number of steps. GRaSS may then calculate some statistical values with given confidence intervals.
GROOVE [28] supports the modeling of objectoriented systems, with graph transformations as a basis for model transformation and operational semantics. Systems thus defined may then be verified using model checking. CheckVML does something similar, although in this case system specifications into a toolindependent abstract representation of transition systems, from which Promela specifications are generated to model check using Spin.
Several attempts to reduce the complexity of model checking have also been proposed. Isenberg et al. propose in [18] the use of bounded model checking via SMT solving. Yousefian et al. use genetic algorithms in [41] to search specific states in large state spaces.
Based on ideas from Event Scheduling, de Lara et al. propose in [12] an interesting way of adding explicit time to graph transformation rules by scheduling rules in the future. Basically, they schedule all possible matches of rules (what they call events) and proceed by handling each of these events. To avoid the explosion in the number of matches, they use a control graph which establishes the possible sequences in which the rules may be applied. This idea could be an alternative way of guaranteeing the absence of unquantified nondeterminism, although at the cost of providing the control graph.
6 Conclusions
We have presented how the eMotions tool has been extended so that the models built conforming to userdefined DSMLs are suitable for statistical model checking. eMotions models are transformed into Maude specifications satisfying the requirements of the PVeStA tool [3], making them suitable to be stochastically analyzed. We have illustrated the use of eMotions to model systems and its statistical model check with a very simple application for message delivery.
With our approach we provide statistical model checking capabilities to userdefined DSMLs in a userfriendly graphical environment. Statistical model checking offers a completely automatic procedure, with the possibility of adjusting the desired confidence interval and error bound.
Although the basic functionality and tooling is already available, much work remains ahead. For example, we would like to automate the check of the satisfaction of the nonquantifiednondeterminism requirements. eMotions features like periodicity, scheduling, or nondegenerate intervals are not yet supported. Moreover, although the response times obtained with PVeStA are acceptable, we would like to explore the possibility of using more powerful model checkers as backend tools. Finally, we will complete the graphical representations of the obtained distributions of results inside our Eclipse plugin.
Footnotes
 1.
eMotions got an “ease of use” award at the 7th Transformation Tool Contest [26].
 2.
Ecore is equivalent to the EMOF (Essential MOF) portion of MOF defined in the MOF 2 specification [25].
 3.
In eMotions, all structural features are qualified with the name of the class they belong to, and all elements are qualified with the name of the metamodel they are defined in. All these qualifications have been removed to improve readability.
 4.
Critical pair analysis is available in Maude, and has been used for tools like its confluence and coherence checkers (see [15]).
Notes
Acknowledgements
This work was partially supported by Research Project TIN201452034R and by Universidad de Málaga (Campus de Excelencia Internacional Andalucía Tech).
References
 1.Agha, G., Greenwald, M., Gunter, C.A., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of DOS using probabilistic rewrite theories. In: Proceedings of FCS (2005)Google Scholar
 2.Agha, G., Meseguer, J., Sen, K.: PMaude: rewritebased specification language for probabilistic object systems. In: Proceedings of the QAPL, ENTCS, vol. 153, pp. 213–239 (2006)Google Scholar
 3.AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 4.Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL  a tool suite for automatic verification of realtime systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)CrossRefGoogle Scholar
 5.Boronat, A., Meseguer, J.: An algebraic semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 377–391. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 6.Boronat, A., Meseguer, J.: MOMENT2: EMF model transformations in Maude. In: Proceedings of JISBD, pp. 178–179 (2009)Google Scholar
 7.Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theoret. Comput. Sci. 236(1–2), 35–132 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
 8.Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: Modelling and analyzing adaptive selfassembly strategies with Maude. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 118–138. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 9.Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAALSMC: statistical model checking for priced timed automata. EPTCS 85, 1–16 (2012). Proceedings of QAPLCrossRefGoogle Scholar
 10.Clavel, M., Durán, F., Eker, S., Lincoln, P., MartíOliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theoret. Comput. Sci. 285(2), 187–243 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
 11.Clavel, M., Durán, F., Eker, S., Lincoln, P., MartíOliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
 12.de Lara, J., Guerra, E., Boronat, A., Heckel, R., Torrini, P.: Domainspecific discrete event modelling and simulation using graph transformation. Softw. Syst. Model. 13(1), 209–238 (2014)CrossRefzbMATHGoogle Scholar
 13.de Lara, J., Vangheluwe, H.: AToM: a tool for multiformalism and metamodelling. In: Kutsche, R.D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 174–188. Springer, Heidelberg (2002)CrossRefGoogle Scholar
 14.Durán, F., Lucas, S., Marché, C., Meseguer, J., Urbain, X.: Proving operational termination of membership equational programs. HigherOrder Symbol. Comput. 21(1–2), 59–88 (2008)CrossRefzbMATHGoogle Scholar
 15.Durán, F., Meseguer, J.: On the ChurchRosser and coherence properties of conditional ordersorted rewrite theories. J. Log. Algebr. Program. 81(7–8), 816–850 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
 16.Eckhardt, J., Mühlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering. LNCS, vol. 7212, pp. 78–93. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 17.Heckel, R., Lajios, G., Menge, S.: Stochastic graph transformation systems. In: Ehrig, H., Engels, G., ParisiPresicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 210–225. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 18.Isenberg, T., Steenken, D., Wehrheim, H.: Bounded model checking of graph transformation systems via SMT solving. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 178–192. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 19.Jansen, D.N., Katoen, J.P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 69–85. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 20.Kelly, S., Tolvanen, J.P.: DomainSpecific Modeling: Enabling Full Code Generation. Wiley, New York (2008)CrossRefGoogle Scholar
 21.Caskurlu, B.: Model driven engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286–298. Springer, Heidelberg (2002)CrossRefGoogle Scholar
 22.Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52–66. Springer, Heidelberg (2002)CrossRefGoogle Scholar
 23.Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic realtime systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 24.Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
 25.Meta object facility (MOF) core specification, Version 2.4.1 (2013)Google Scholar
 26.MorenoDelgado, A., Durán, F.: The movie database case: a solution using the Maudebased eMotions tool. In: 7th Transformation Tool Contest (TTC), vol. 1305, pp. 116–124. CEUR Workshop Proceedings (2014)Google Scholar
 27.Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of RealTime Maude. HigherOrder Symbol. Comput. 20(1–2), 161–196 (2007)CrossRefzbMATHGoogle Scholar
 28.Rensink, A.: The GROOVE simulator: a tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 29.Rivera, J.E., Durán, F., Vallecillo, A.: A graphical approach for modeling timedependent behavior of DSLs. In: Proceedings of VL/HCC, pp. 51–55. IEEE (2009)Google Scholar
 30.Rivera, J.E., Durán, F., Vallecillo, A.: On the behavioral semantics of realtime domain specific visual languages. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 174–190. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 31.Rivera, J.E., Vallecillo, A., Durán, F.: Formal specification and analysis of domain specific languages using Maude. Simulation 85(11/12), 778–792 (2009)CrossRefGoogle Scholar
 32.Romero, J.R., Rivera, J.E., Durán, F., Vallecillo, A.: Formal and tool support for model driven engineering with Maude. J. Object Technol. 6(9), 187–207 (2007)CrossRefGoogle Scholar
 33.Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformations: Volume 1 Foundations. World Scientific, River Edge (1997)zbMATHGoogle Scholar
 34.Schmidt, Á., Varró, D.: CheckVML: a tool for model checking visual modeling languages. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 92–95. Springer, Heidelberg (2003)CrossRefGoogle Scholar
 35.Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of blackbox probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 36.Sen, K., Viswanathan, M., Agha, G.A.: VeStA: a statistical modelchecker and analyzer for probabilistic systems. In: Proceedings of QEST, pp. 251–252. IEEE (2005)Google Scholar
 37.Taentzer, G.: AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446–453. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 38.Torrini, P., Heckel, R., Ráth, I.: Stochastic simulation of graph transformation systems. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 154–157. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 39.Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 40.Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)CrossRefGoogle Scholar
 41.Yousefian, R., Rafe, V., Rahmani, M.: A heuristic solution for model checking graph transformation systems. Appl. Soft Comput. 24, 169–180 (2014)CrossRefGoogle Scholar