=Paper=
{{Paper
|id=Vol-2019/exe_4
|storemode=property
|title=Towards One Model Interpreter for Both Design and Deployment
|pdfUrl=https://ceur-ws.org/Vol-2019/exe_4.pdf
|volume=Vol-2019
|authors=Valentin Besnard,Matthias Brun,Philippe Dhaussy,Frédéric Jouault,David Olivier,Ciprian Teodorov
|dblpUrl=https://dblp.org/rec/conf/models/BesnardBDJOT17
}}
==Towards One Model Interpreter for Both Design and Deployment==
https://ceur-ws.org/Vol-2019/exe_4.pdf
Towards one Model Interpreter for
Both Design and Deployment
Valentin Besnard∗ , Matthias Brun∗ , Philippe Dhaussy† , Frédéric Jouault∗ , David Olivier‡ , and Ciprian Teodorov†
∗ TRAME team, ESEO, Angers, France, firstname.lastname@eseo.fr
† Lab-STICC UMR CNRS 6285, ENSTA Bretagne, Brest, France, firstname.lastname@ensta-bretagne.fr
‡ Davidson Consulting, Rennes, France, david.olivier@davidson.fr
Abstract—Executable modeling of complex embedded systems more complex the interpretation of diagnosis results. On the
is essential for bug discovery and safety validation at early design other hand, it is relatively difficult to prove the equivalence
stages. A relatively large number of tools enable early design between all these models because each one is defined in terms
diagnosis and validation by transforming and analyzing the
model into a formal setting. However, this transformation induces of a different language with different semantics. In summary,
a semantic gap rendering diagnosis more difficult. Moreover, on we notice that the root cause of these problems is the use
the way to deployment, executable models are transformed into of multiple definitions of the language semantics defined by
low level executable code. Existence of this second transformation transformations towards different formalisms.
similarly renders diagnosis of the deployed system more difficult,
and also increases validation costs of the approach in the context
of critical systems: a non trivial equivalence relation needs to To solve these issues, we propose an approach based on
be established between the formally analyzed model and the a single semantics definition that overcomes the equivalence
executable code. In this paper, we introduce a first step towards issue and guarantees the absence of semantic gap. Trans-
addressing these problems with a bare-metal UML interpreter, formations that modify the semantics should be avoided to
which uniquely defines the executable semantics for both design preserve the uniqueness of this definition. In fact, our solution
and deployment. To facilitate the diagnosis and validation process
our interpreter offers a diagnosis interface through which the consists of using a unified semantics for both design and
semantics is shared with diagnosis tools. The tools rely on this deployment. This unique definition has been implemented in
interface to interact with (observe and control) the executing a bare-metal interpreter of models. To ensure executability of
model either locally on a PC during early design phases or these models, the selected semantics should be complete and
remotely on the target embedded system after deployment. We without inconsistencies. For this interpreter, we have chosen
illustrate our approach on a railway level crossing system ported
to two embedded targets (at91sam7s and stm32), to which we tUML [2, 3], a textual notation for a subset of UML, that
connect a remote high-level simulator for interactive execution fits these requirements. This interpreter enables to execute
control and exhaustive state-space exploration. software applications at a higher level of abstraction. While
Index Terms—UML, Model Interpretation, Model Verification, this approach solves semantic issues, a lack of diagnosis tools
Embedded Systems. appears. To fix this problem, our idea is to share the unified
semantics of the language with diagnosis tools (e.g., simulator,
I. I NTRODUCTION debugger). A generic communication interface enables the
The new generation of embedded systems and CPS (Cyber- connection of these tools to the interpreter to observe and
Physical Systems) provides more powerful features to meet control model execution.
emerging needs in numerous fields (e.g., automotive, avionics,
robotics, smart cities). With the development of IoT (Internet Experimentations performed on a railway level crossing sys-
of Things), they now tend to be connected and to collaborate tem show that our approach is on the way towards feasibility.
with other systems on networks. This increasing complexity Our UML execution engine can be deployed on a PC (to be
creates more difficulties for engineers to check and ensure used during the design phase) as well as on two embedded
safety, or simply to avoid bugs. Not only are behaviors of these targets: at91sam7s and stm32. To control the interpreter, a
systems more uncertain but they are also more vulnerable to communication link has been developed to connect different
cyber attacks, due to their network connections. To prevent diagnosis tools. For the moment, we have a simulator that
the introduction of bugs during development of such systems, enables users to observe and control the execution of the
there is a need to execute, simulate, and verify models. model. We illustrate this feature by computing the exhaustive
In the industrial world, the common approach [1] consists state-space of the level crossing model.
of two transformations: one that converts the design model
into various models (e.g., formal models) used by diagnosis The paper is organized as follows. Section II presents our
tools during the design phase, and another one that generates approach and our main contribution: a bare-metal UML model
deployable code from the user model. interpreter. In Section III, we show results of our experimen-
This common approach has two main issues. On the one tations on the level crossing example. Finally, related works
hand, the semantic gap created by transformations renders are discussed in Section IV and we conclude in Section V.
Figure 1. Diagram of the classical approach
Figure 3. Class diagram of the interpreter
to adapt the syntax of the model without changing the seman-
Figure 2. Diagram of our approach using a model interpreter tics. This operation is a direct transliteration of each element
of the model into C language as struct initializers, nothing
more. Afterwards, this executable model can be executed by
II. D ESIGN OF A BARE -M ETAL UML I NTERPRETER the model interpreter. One thing we still need to establish is
A. Approach Overview the determinism of the interpreter execution (i.e., the absence
Our approach introduces an interpreter of UML models of undefined behaviors [4]). This could be validated with static
implemented in C language, which has the specificity to use or dynamic analysis of the interpreter code.
a single definition of the semantics for both the design phase This interpreter solves the three main drawbacks of the com-
and the execution. To perceive the innovative aspect of this mon approach. Firstly, the problem of equivalence between
technique, it is important to understand the common approach the design model and the code has been overcome thanks to
used by engineers to develop software systems (Figure 1). the single definition of the semantics. Secondly, the semantic
First of all, engineers model the system using the semantics gap has been removed because no transformation, which
definition of dedicated modeling languages (e.g., UML, fUML, alters or changes the semantics, is used. Thirdly, this unique
SysML). At this stage, many diagrams are typically produced definition facilitates the understanding of diagnosis results in
to describe the system under multiple points of view. Some of terms of design model concepts. This solution has also other
them are dedicated to system execution while others are used advantages. It may contribute to save time during the design
for alternative purposes (e.g., testing, engineers understanding phase by modeling only needed points of view of the system.
of the system). Diagrams required for execution are trans- Like code generation, the coding step requires no effort and
formed into code using manual or automatic code generation. the risk to introduce bugs is reduced. In our approach, this
This transformation may change the semantics definition of the goal will be addressed by simulating and deploying the model
model and creates a semantic gap between the design model directly on the interpreter embedded on the target.
and the code. Hence, it is more difficult to identify an element Nevertheless, the execution of a DSL like tUML, introduced
of the design model in code and conversely. In parallel of this in [2, 3], creates another issue. Indeed, a lack of diagnosis
first activity, the design model is also transformed into other tools (e.g., simulator, model-checker, debugger, or profiler)
formalisms to be used by diagnosis tools for different purposes can be noticed for some specific languages. Rather than
(e.g., simulation, exploration, formal verification). With this implementing an ad-hoc toolbox for each DSL, a solution
second transformation, a new issue appears. It is now more (Figure 2) is to link the interpreter with existing tools [5]. Our
difficult to prove the equivalence between these models used model interpreter has been designed to be controlled remotely
for diagnosis and validation, and the deployed code. through a simple and generic API. This feature enables control
Our approach (Figure 2) consists of modeling a system of model interpretation either step by step or in a back-in-
using the tUML language, that offers a clear and complete def- time way [6–8]. This interface is exactly what is needed
inition of a model without inconsistencies [2, 3]. With tUML, to connect a model-checker, like LTSmin [9] or tools from
three views of the system are needed to define an executable ENSTA Bretagne [10, 11], for formal properties verification.
model: class diagram, state machines, and composite structure
diagram. Then, this model is serialized to C to be loaded into B. Interpreter Design
the interpreter. The serialization is applied only to elements The model interpreter introduced in this paper has been
needed for the execution (i.e., runtime data and runtime code) implemented in C, a low level and general purpose language
perfectly suited for embedded systems. The goal of this C. Communication Interface
interpreter is to define a unique semantics definition that will
be used for both design and deployment, and to execute models
according to this semantics. To solve the problem of the lack of diagnosis tools with
DSLs, we take into account the possibility to connect the
interpreter with existing tools (e.g., simulator, debugger, pro-
We will now give an overview of the interpreter architecture filer, model-checker). Our idea is to provide a generic API to
(Figure 3) rather than a detailed description that exceeds the be able to control remotely the execution of the interpreter.
scope of this article. The Interpreter class is composed of a This simple interface is composed of four requests. Get
collection of ActiveObjects and of the user model conformant configuration: collects the current configuration (memory
to the tUML semantics. tUML basically corresponds to a state) of the interpreter. A configuration is composed of the
subset of the class, state machines, and composite structure current state, the EventPool and values of attributes, of each
diagrams from UML. This last diagram defines a composite ActiveObject. Set configuration: loads a configuration as
class, called SUS (for System Under Study), which goal is the current memory state of the interpreter. Get fireable
to specify the part played by each ActiveObject as well as transitions: gets transitions from ActiveObject instances that
links between them. Every ActiveObject has a state machine have their trigger and their guard satisfied in the current state.
that defines its behavior, the current state of its state machine, A fireable transition is identified by its id and the ActiveObject
and the list of all fireable transitions from its current state. to which it belongs. Fire a transition: fires a fireable
It can compute fireable transitions, and fire a transition to transition of an ActiveObject. When firing, the event of the
make its current state evolve. An ActiveObject also owns an trigger is consumed, the current state is updated, and effects
EventPool to store occurrences of events that it receives. The attached to this transition are processed.
EventPool is currently designed as a bits field, which offers
some advantages (e.g., a bounded representation of events) With only four requests, this simple interface offers several
and defines a particular execution semantics. This specific possibilities. Indeed, the model interpreted can be executed
semantics can be modified by using other data structures (e.g., step by step. A specific execution path can be chosen with
FIFO) to implement different features (e.g., storage of multiple the ”Get fireable transitions” request. This feature enables to
occurrences of a given event, preservation of events reception check a property or find a bug in a specific path. However, the
order). The EventPool has three principal operations: one to most powerful functionality is the ability to make back-in-time
signal an event, one to consume an event, and the last one execution [6–8]. The ”Set configuration” request can place or
to check if an event has occurred. An ActiveObject also has replace the interpreter in any configuration. This feature can
a Store where values of its attributes are stored. The Store be useful for debugging if we want to come back on previous
has only two operations: one to assign a value to an attribute, configurations but also for the exploration of the state-space.
and another to get the value of an attribute. To have a generic This generic API gives the possibility to use several kinds
representation of attributes, we used a generic pointer, which of tools in an easy way. Indeed, to connect an existing tool,
points to the suitable value of the attribute, and an integer to you just need to add a TCP client and to implement the
store the size of its data type. Furthermore, an ActiveObject communication interface. In our point of view, it is better to
needs to evaluate guards on transitions of its state machine. use existing tools than implementing ad-hoc tools. One reason
The class GuardEval has been designed for this purpose. is that existing tools have been tested, used and approved for
Currently this class involves Flex and Bison to parse guard many years. Engineers are familiar with these tools and no
expressions, but future works will improve that evaluation formation will be required to teach them how to use them.
using offline preprocessing to reduce the memory footprint
Our interpreter can support multiple kinds of connections
and enhance execution performances. The last class is the
even if only TCP connection for PC, and RS232 connection
EffectBehavior that executes effects associated to transitions
for at91sam7s and stm32 have been developed for the moment.
when one of them is fired. Two kinds of effects are available
With a strategy pattern [12], only the code of the chosen con-
yet with the simplified version of the ABCD language [3] used
nection is compiled and loaded in the target, which contributes
here. It is possible to send events to another ActiveObject or
to reduce memory footprint. A new kind of connection can
to assign a value to an attribute.
be easily added by implementing the connection interface.
The interpreter should only know how to open, read, write
This interpreter has been designed to be portable on differ- and close the connection. It is important for us to offer this
ent targets. At the moment, this interpreter can be executed functionality because embedded boards have sometimes few,
on a PC but is also supported on two embedded targets: and specific kinds of serial ports available. Furthermore, to
at91sam7s and stm32. Other targets could be easily added avoid implementing a serial communication within an existing
because we designed the interpreter to be linked with target- tool, we have created a little application that converts TCP data
specific libraries of the chosen target at build time. This frames into serial data frames. With this converter, only a TCP
specificity helps to fit embedded systems requirements, which client plugin needs to be implemented into a tool so that it can
involve limited computation and memory resources. control the interpreter over any serial connection.
Figure 4. Schema of the level crossing example
Figure 5. Composite structure diagram of the level crossing example
III. A UML M ODEL ON AN E MBEDDED TARGET
A. Case Study
To illustrate our approach we use a level crossing system,
presented in Figure 4. A level crossing is a system built at
the intersection of a railroad and a road. It is responsible for
ensuring the safety of all road users during the passage of the
train. In this case study, a UML model of a level crossing
has been designed (Figure 5 and Figure 6). The Controller Figure 6. State machines of the level crossing example
controls the activation of the RoadSign (e.g, lights, alarm)
and the closure of the Gate according to signals received
from TrackCircuits. TrackCircuits are sensors able to detect triggers sequentially the detection of the entrance TrackCircuit
the Train on the railroad. Each one sends a signal when the (tcEntrance), of the approach TrackCircuit (tcApproach) and
Train is detected and another one when the detection ends. The of the exit TrackCircuit (tcExit). This linear state machine
level crossing counts three TrackCircuits: one for the entrance, considers the passage of a single train on the level crossing.
one for the approach, and one for the exit of the level crossing. TrackCircuits state machines have only two states Detection
All these objects are active, so their behaviors are described and NoDetection that transmit signals to the controller at the
by state machines. A state machine is composed of states beginning and at the end of train detection. State machines
linked together with directed transitions. Transitions can be for tcApproach and tcExit are similar to the state machine
fired to change the state of an ActiveObject. A transition of tcEntrance presented on Figure 6. The Controller state
is fireable if the event associated with its trigger has been machine has the most important role in the system. When
received by this state machine and if its guard is satisfied. the train is detected by tcEntrance, it is in charge of sending
When a transition is fired, its effect is processed. The language a signal to switch on lights of the roadSign. Then, it sends a
used to parse guards defined as OpaqueExpressions and effects signal to close the gate when the train begins to be detected
defined as OpaqueBehaviors is a simplified version of ABCD by tcApproach. At the end of the detection, we consider that
[3]. The current version of the interpreter supports simple the train is passing until the detection of tcExit, which sends a
boolean expressions for guards as well as the sending of events signal to open the gate. Finally, a signal is send to switch off
and assignment of variables for effects. This is sufficient to lights of the roadSign when the train quits the detection zone
execute a model and make ActiveObjects interact together. of tcExit, and the controller returns in its idle state. The state
We will now describe behaviors of ActiveObjects (Figure 6) machine of the RoadSign can alternate between Inactive and
to better understand these interactions. The Train state machine Active states thanks to switchOn and switchOff signal events.
Figure 7. User interface of the remote execution controller Figure 8. Graph of the state-space exploration of the level crossing example
In the same way, the state machine of the Gate is driven by communication unit developed in the simulator has been inte-
open and close events to go in the Opened or Closed state. grated into this state-space explorer. This tool has computed
This example model is not connected with its real envi- the state-space of the level crossing model using a breadth first
ronment because the link of the interpreter with inputs and search algorithm connected with the interpreter via the TCP
outputs of the embedded board have not been implemented diagnosis interface. This results in a state-space constituted of
yet. However, the level crossing of our case study has sensors 1,825 different configurations linked to one another with 5,793
(TrackCircuits) and actuators (RoadSign and Gate) that have transitions (This state-space exploration has been performed
been integrated to the design model. This enables to simulate with 3 events preloaded in the EventPool of the controller:
the level crossing example as if it was executing on the real entranceBegin, exitBegin, and exitEnd.). The associated state-
system, which uses inputs and outputs of the board. In fact, space graph shown in Figure 8 gives an overview of the extent
only the controller will need to be deployed on the real system of this model exploration.
because other entities are active elements of the environment. To sum up, these experimentations show the ability of our
interpreter to be remotely controlled by diagnosis tools for
B. Deployment and Results simulation and exploration purposes.
The level crossing case study has been deployed on our
interpreter of UML models. This experimentation has been IV. R ELATED W ORK
made on a PC with a Linux operating system, and on both Some generic tools are able to build an interpreter, and
at91sam7s and stm32 targets without operating systems (bare- execute models designed with a given DSL. GEMOC studio
metal). The level crossing model has been designed using is an Eclipse plugin that integrates a language workbench,
tUML before being serialized into Eclipse UML, and finally and a modeling workbench to define a DSML as well as
into C. It has been successfully executed on the interpreter design models conforming to this language. This environment
by firing the first fireable transition on active objects in can be used to build a model interpreter, and other diagnosis
turns. Without any optimizations, the memory footprint of the tools (e.g., a graphical model animator, a trace manager) [13].
binary executable file containing the model, the interpreter, Another example is the K framework [14], an executable
and specific libraries of the board for the stm32 is only 131 semantics framework based on rewriting rules. It can be
ko, which is sufficiently small to be embedded. used to define programming languages or create tools. The
We have also connected two diagnosis tools to control possibility to target a large number of languages is a significant
remotely the execution of the level crossing model. A sim- advantage of these frameworks. However, this also induces a
ulator has been developed to explore some execution paths lack of performance because the implementation is not specif-
of this model. It can be connected to the interpreter using ically adapted to the application. Contrary to these tools, our
either a TCP connection or a serial connection. Indeed, a interpreter has been designed in a classical way but with the
serial port communication using a UART peripheral of the goal to fit requirements of embedded systems. Our approach
PC was developed to communicate directly with the embedded takes also into account that the interpreter has to be connected
interpreter for debug purpose but this functionality has become to existing diagnosis tools rather than generated new ones
useless with the communication converter. The simple user for each DSML. Some alternative methods (e.g., [1, 15–17])
interface (Figure 7) provides four buttons to apply each request focus on a semantics definition based on state machines. The
of the API and directly control the model execution. This transformation of these diagrams into intermediate formalisms
gives the possibility to the user to get information on the like EHA enables the direct execution of these state machines.
execution and to make the model evolve by firing transitions. These tools are mainly used for simulation [18], exploration
To observe the model execution, the simulator has also the [19] and model-checking [1] purposes. However, they do
ability to decode the configuration and to display its content not defined a generic interface of communication like our
in an understandable way for humans. interpreter and it is not possible to control their execution on an
Another diagnosis tool has also been connected to the model embedded target. The key point of our approach is the use of a
interpreter for state-space exploration. For this purpose, the single semantics definition, which fixes the equivalence issue
between design model and code. This could also be achieved [10, 11] to verify formal properties directly on models ex-
using verified compilers or interpreters (e.g., the CompCert ecuted by the interpreter on embedded boards. We are also
C compiler [20], and Jitk [21]). The formal language Coq interested in interfacing other diagnosis tools for several
enables to check and certify formal properties of programming purposes: monitoring, debugging, and profiling.
languages. Correctness of generated or interpreted code is R EFERENCES
formally proven. It ensures this way the equivalence of the
[1] G. Pintér and I. Majzik, “Program Code Generation based on UML
design model with the code. However, this kind of tools is not Statechart Models,” Periodica Polytechnica, vol. 47, no. 3–4, pp. 187–
widely used yet due to its complexity. 204, 2003.
Another essential problem for the execution of models is [2] F. Jouault and J. Delatour, “Towards Fixing Sketchy UML Models
by Leveraging Textual Notations: Application to Real-Time Embedded
the lack of tools after deployment. This issue has not been Systems,” in OCL 2014, A. D. Brucker, C. Dania, G. Georg, and
completely addressed yet. For UML, some simulators and M. Gogolla, Eds., vol. 1285, Valencia, Spain, Sep. 2014, pp. 73–82.
interpreters begin to appear without being widely used at the [3] F. Jouault, C. Teodorov, J. Delatour, L. Le Roux, and P. Dhaussy, “Trans-
formation de modèles UML vers Fiacre, via les langages intermédiaires
moment. For other DSLs, only generic frameworks or the use tUML et ABCD,” Génie logiciel, vol. 109, p. xx, Jun. 2014.
of a design pattern dedicated for monitoring [5] are able to [4] J. Regher, “A guide to undefined behaviours in c and c++,” 2010.
generate this kind of tools. We differentiate our interpreter by [5] Z. Drey and C. Teodorov, “Object-oriented design pattern for dsl
program monitoring,” in Proceedings of SLE 2016. New York, NY,
the use of a generic interface to connect it with existing tools. USA: ACM, 2016, pp. 70–83.
Numerous related works have also been achieved on real [6] E. Bousse, J. Corley, B. Combemale, J. Gray, and B. Baudry, “Sup-
porting efficient and advanced omniscient debugging for xdsmls,” in
time virtual machines (VMs) [22–25]. Several concepts used Proceedings of SLE 2015, New York, USA, 2015, pp. 137–148.
by researchers on this topic have been applied to DSL ex- [7] J. Corley, B. P. Eddy, E. Syriani, and J. Gray, “Efficient and scalable
ecution engines. All these VMs interpret bytecode, so one omniscient debugging for model transformations,” Software Quality
Journal, vol. 25, no. 1, pp. 7–48, Mar 2017.
important difference is that our model interpreter provides a [8] S. V. Mierlo, Y. V. Tendeloo, S. Mustafiz, and B. Barroca, “Debugging
higher level of abstraction. Some of these VMs have been parallel devs,” 2014.
implemented using specific languages (e.g., Estérel [26]). In [9] G. Kant, A. Laarman, J. Meijer, J. Pol, S. Blom, and T. Dijk, “Ltsmin:
High-performance language-independent model checking,” in Proceed-
comparison with our interpreter, UML is more adapted to ings of the 21st International Conference on Tools and Algorithms for
model systems. Furthermore, UML is widely used during the the Construction and Analysis of Systems - Volume 9035. New York,
design phase of systems in the industrial world. Using the NY, USA: Springer-Verlag New York, Inc., 2015, pp. 692–707.
[10] C. Teodorov, P. Dhaussy, and L. Le Roux, “Environment-driven reach-
same language for the design phase and the code is better ability for timed systems,” International Journal on Software Tools for
because no semantic gap is created. Virtual machines for Technology Transfer, vol. 19, no. 2, pp. 229–245, Apr 2017.
sensor networks (e.g., Maté [27], and Mote runner [28]) have [11] C. Teodorov, L. Le Roux, Z. Drey, and P. Dhaussy, “Past-free[ze]
reachability analysis: reaching further with dag-directed exhaustive state-
similarities with our work even if our approach is more focused space analysis,” Software Testing, Verification and Reliability, vol. 26,
on industrial applications with both sensors and actuators. no. 7, pp. 516–542, 2016, stvr.1611.
Nevertheless, VMs for sensors networks face several issues [12] E. Gamma, Design patterns: elements of reusable object-oriented soft-
ware. Pearson Education India, 1995.
especially on communication speed and execution that we will [13] B. Combemale, J. Deantoni, O. Barais, A. Blouin, E. Bousse, C. Brun,
also need to solve for making our interpreter scalable. T. Degueule, and D. Vojtisek, “A Solution to the TTC’15 Model
Execution Case Using the GEMOC Studio,” in 8th Transformation Tool
Contest. l’Aquila, Italy: CEUR, 2015.
V. C ONCLUSION [14] G. Roşu and T. F. Şerbănuţă, “An overview of the K semantic frame-
work,” Journal of Logic and Algebraic Programming, vol. 79, no. 6, pp.
In this paper, we have introduced an interpreter of UML 397–434, 2010.
models with the specificity to use a single semantics definition [15] T. Schattkowsky and W. Muller, “Transformation of uml state machines
for direct execution,” in Proceedings of the 2005 IEEE Symposium on
for both the design phase and the deployment. This approach Visual Languages and Human-Centric Computing. Washington, DC,
eliminates the problem of the equivalence between models, USA: IEEE Computer Society, 2005, pp. 117–124.
and the semantic gap created by model transformations. The [16] G. Pintér and I. Majzik, “Automatic Code Generation Based on Formally
Analyzed UML Statechart Models,” in Proceedings of the FORMS-2003
use of tUML enables to define complete executable models Conference, G. Tarnai and E. Schnieder, Eds. Budapest, Hungary:
that can be directly executed on the interpreter by serializing LH́armattan, May 15-16 2003, pp. 45–52.
the model into C language. A first step to solve the lack of [17] E. Cariou, C. Ballagny, A. Feugas, and F. Barbier, “Contracts for model
execution verification,” in Proceedings of the 7th European Conference
diagnosis toolboxes for DSLs has been made with the imple- on Modelling Foundations and Applications. Berlin, Heidelberg:
mentation of a generic communication interface that enables Springer-Verlag, 2011, pp. 3–18.
the use of existing tools. This enables to control remotely the [18] A. Kirshin, D. Dotan, and A. Hartman, A UML Simulator Based on a
Generic Model Execution Engine. Springer Berlin Heidelberg, 2007,
execution of the interpreter step by step or in a back-in-time pp. 324–326.
way. We illustrate this functionality by implementing a simple [19] D. Riehle, S. Fraleigh, D. Bucka-Lassen, and N. Omorogbe, “The
simulator that communicates with the interpreter running on architecture of a uml virtual machine,” in Proceedings of OOPSLA ’01.
New York, NY, USA: ACM, 2001, pp. 327–341.
an embedded board. This simulator can be used to simulate [20] X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, “The CompCert
a model and to explore some execution paths. We have also Memory Model, Version 2,” INRIA, Research Report 7987, Jun. 2012.
confirmed that we can explore a full state-space. [21] X. Wang, D. Lazar, N. Zeldovich, A. Chlipala, and Z. Tatlock, “Jitk:
A trustworthy in-kernel interpreter infrastructure,” in Proceedings of the
Future work will focus on linking this engine with the 11th USENIX Conference on Operating Systems Design and Implemen-
LTSmin [9] model-checker and tools from ENSTA Bretagne tation. Berkeley, CA, USA: USENIX Association, 2014, pp. 33–47.
[22] J. Auerbach, D. F. Bacon, B. Blainey, P. Cheng, M. Dawson, M. Fulton,
D. Grove, D. Hart, and M. Stoodley, “Design and implementation of
a comprehensive real-time java virtual machine,” in Proceedings of the
7th ACM &Amp; IEEE International Conference on Embedded Software.
New York, NY, USA: ACM, 2007, pp. 249–258.
[23] A. Armbruster, J. Baker, A. Cunei, C. Flack, D. Holmes, F. Pizlo, E. Pla,
M. Prochazka, and J. Vitek, “A real-time java virtual machine with
applications in avionics,” ACM Trans. Embed. Comput. Syst., vol. 7,
no. 1, pp. 5:1–5:49, Dec. 2007.
[24] J. Baker, A. Cunei, C. Flack, F. Pizlo, M. Prochazka, J. Vitek, A. Arm-
bruster, E. Pla, and D. Holmes, “A real-time java virtual machine for
avionics - an experience report,” in Proceedings of the 12th IEEE
Real-Time and Embedded Technology and Applications Symposium.
Washington, DC, USA: IEEE Computer Society, 2006, pp. 384–396.
[25] D. Simon and C. Cifuentes, “The squawk virtual machine: JavaTM on
the bare metal,” in Companion to the ACM SIGPLAN OOPSLA ’05
Conference. New York, NY, USA: ACM, 2005, pp. 150–151.
[26] B. Plummer, M. Khajanchi, and S. A. Edwards, “An esterel virtual
machine for embedded systems,” in Proceedings SLAP ’06, vol. 126,
Vienna, Austria, 2006, pp. 912–917.
[27] P. Levis and D. Culler, “Maté: A tiny virtual machine for sensor
networks,” SIGPLAN Not., vol. 37, no. 10, pp. 85–95, Oct. 2002.
[28] A. Caracas, T. Kramp, M. Baentsch, M. Oestreicher, T. Eirich, and
I. Romanov, “Mote runner: A multi-language virtual machine for small
embedded devices,” in Proceedings of the 2009 Third International
Conference on Sensor Technologies and Applications. Washington,
DC, USA: IEEE Computer Society, 2009, pp. 117–125.