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.