Executable Domain Specific Modeling Languages (xDSML) opens many possibilities in terms of early verification and validation (V&V) of systems, including the use of dynamic V&V approaches. Such approaches rely on the notion of execution trace, i.e. the evolution of a system during a run. To benefit from dynamic V&V approaches, it is therefore necessary to characterize what is the structure of the executions traces of a given xDSML. Our goal is to provide an approach to design trace metamodels for xDSMLs. We identify seven problems that must be considered when modeling execution traces, including concurrency, modularity, and scalability. Then we present our envisioned approach to design scalable multidimensional trace metamodels for xDSMLs. Our work in progress relies on the dimensions of a trace (i.e. subsets of mutable elements of the traced model) to provide an original structure that faces the identified problems, along with a trace API to manipulate them.
In the recent years, a lot of effort have been made to provide tools and methods
to design executable Domain Specific Languages (xDSMLs) [
A central concept in dynamic V&V approaches is the execution trace, which represents the evolution of a system during a run. A trace is the alternate sequence of states of the system and events that triggered the state changes. All previously cited approaches rely on traces: model checking consists in verifying a property of a system by analyzing all its possible traces, and a counter-example in the form of a trace is provided if it is not satisfied; runtime verification consists in checking whether or not a trace satisfies a property; debuggers require traces to be able to replay faulty scenarios in order to investigate for bugs.
Henceforth, a significant prerequisite for the V&V of executation models is
the definition of the structure of the execution traces of a considered xDSML.
Since an xDSML should define what is the state (also called runtime data) of
a model during its execution [
A status
Initial area
Final area A sewnhdesncmooorvdiinngates A nitoctiafinesmBovtehat
Moving towards final area B status
Initial area
Moving towards final area
B sends coordinates when moving
Final area
Our motivating example consists in an xDSML called RoboML, which extends timed automata with hierarchy, events, and domain specific actions. A RoboML model consists in a set of communicating timed automata. When executed, the current state of the automata changes depending on the current state, events, clocks and conditions. Additional domain-specific runtime data is available, such as the GPS coordinates of the robot. Actions triggered on transitions allow a robot to move, interact and communicate with other robots. The very simple scenario we consider is based on two robots A and B, each configured with a RoboML model. Robots are configured to regularly send their coordinates to the other robot when they change their position. Figure 1 illustrates the scenario, which can be summed up in the following way:
In this section, we present a series of problem that must be dealt when modeling execution traces, and we illustrate them with the example introduced in the previous section. 3.1
The first category of problems concerns the contents of an execution trace, apart from the state of the executed model and the events that triggered state changes. (Pb. 1) Concurrency modeling The execution of one or multiple models may imply concurrent variables within runtime data. In such case, the different states of these variables may or may not be independent from one another. In our example, the status of a robot is most of the time completely independent from the status of the other. However, communications between the robots imply some kind of ordering between the states of the robots. For instance, we know that B didn’t start moving before receiving a message from A, thus allowing us theoretically to verify property (a). A challenge is thus to take into account these concurrency relationships between variables into the trace structure. (Pb. 2) User-defined additional information Analyzing the behavior of a system requires information about how it changes over time. Yet, in some cases, properties may concern data that we do not directly have. In our example, property (b) concerns the meters covered by a robot, which is not directly available in the state of the executed model. Such variable could easily be derived from the evolution of the coordinates of the robot and would belong in the trace to verify such properties. (Pb. 3) Scalability in space Execution traces can be arbitrarily large, as some complex systems are monitored continuously in case a failure occurs. Thus a challenge is to manage scalability in space when manipulating traces, whether it is offline (file or database storage) or online (in memory). In our example, a robot changes its internal state all the time to update its coordinates or listen to communications, leading quickly to a large amount of states. 3.2
The second category of problems concerns the eventual manipulations of an
execution trace, which may constrain the structure of the trace.
(Pb. 4) Modularity A trace must be constructed during the run of a program,
in order to be manipulated either during or after the run. Modularity of the
trace is a problem for both the construction and the manipulation phases. First,
when tracing a system, one can be interested in observing only a subset of the
variables, which require a non-monolithic and modular trace format. Second,
when manipulating a trace, one might want to extract a subset of the information
(e.g. a subtrace with only a selection of variables), or conversely to add new
information within the trace (e.g. derived variables). In our example, property (a)
only concerns the movement states of the robots and not their coordinates, thus
extracting a trace with only the former information would be relevant to prove
this property.
(Pb. 5) Manipulation safety Generic trace metamodels exist to model all kinds
of traces for any executable language [
In this section, we present the multiple choices we made for our approach to design scalable multidimensional trace metamodels, and how these choices participate in solving the problems stated in the previous section. 4.1
Our approaches relies on an original way to structure execution traces. We illustrate it informally in Figure 2, and we highlight important choices in the following paragraphs.
Multiple dimensions A trace can be defined as a single alternate sequence of
states and events. Yet, it is very likely that only a subset of the variables really
change from a state to another. Our idea is thus to consider multiple dimensions
in a trace, each being a set of mutable elements of the executed model. We then
Robot A
trace
lat=10.3
long=14.2
0.7
define a trace as a set of subtraces, each being the evolution of a specific
dimension within the run. Such structure allow us to solve many problems. First,
by manipulating dimensions separately, we can define concurrency relationships
between them (Pb. 1). More precisely, we consider that states can be linked
by observations (i.e. states that were simultaneous at some point) or
synchronizations (i.e. states that changed simultaneously), while events can be linked
by ordering relationship such as precedence or coincidence (we refer to [
Data sharing For scalability in space (Pb. 3), our idea is to maximize data
sharing among steps of the trace, i.e. reduce redundancy from a step to another.
Our approach relies on ideas of our previous work on scalable model cloning [
Domain specific trace metamodel To provide manipulation safety to trace models (Pb. 5), our solution is to design domain specific trace metamodels, i.e. metamodels each of which defines precisely what are the traces of a single xDSML. This choice ensures that all traces are consistent with regard to the traced language. In addition, we can define the state of a model of a given xDSML without relying on unsafe generic types (e.g. EObject when using the Eclipse Modeling Framework (EMF)). The drawback is that is becomes necessary to provide one trace metamodel per xDSML, but we plan to overcome this by providing a generative approach. 4.2
Generating trace metamodels has multiple advantages as stated in the previous
section. However, the main drawback is that operations defined for a given trace
metamodel are not compatible with a different trace metamodel (Pb. 6).
Following the same trend as recent first-class traces approaches [
Verification and validation of executable models is a challenge that requires the modeling of execution traces. We identified seven problems that must be considered when modeling traces, and we presented our idea of multidimensional traces coupled with a trace manipulation API. Such traces take into account concurrency, scalability, modularity among other aspects. Further work will be the implementation of the approach and its application to RoboML. Acknowledgement. This work is partially supported by the ANR INS Project GEMOC (ANR-12-INSE-0011).