Domain-Specific Model Checking for Cyber-Physical Systems Christopher Gerking and Wilhelm Schäfer Stefan Dziwok and Christian Heinzemann Software Engineering Group Software Engineering Heinz Nixdorf Institute, University of Paderborn Project Group Mechatronic Systems Design, Fraunhofer IPT 33102 Paderborn, Germany 33102 Paderborn, Germany Email: christopher.gerking@upb.de Email: stefan.dziwok@ipt.fraunhofer.de Abstract—Cyber-physical systems (CPS) require model check- for CPS and a model checker have typically large language ing to guarantee the functional correctness of software models, differences. providing counterexamples in case of violations. Domain-specific An approach for applying model checking to DSML models model checking (DSMC) allows to apply model checking to specific application domains. DSMC hides the complexity of using is domain-specific model checking (DSMC, [3]). Its goal is a model checker by translating from a domain-specific modeling to hide the formal models, i.e., the model checker’s input language (DSML) to the model checker’s input language, and by language and the output format of counterexamples. DSMC translating counterexamples back to the domain-specific level. consists of three parts: (i) the forward translation that trans- Implementing DSMC is challenging for CPS due to the large lates the DSML model to the model checker’s input language, differences between DSMLs and the input language of a model checker. In this paper, we present a successful application of (ii) the automated invocation of the model checker, and (iii) the DSMC to M ECHATRONICUML, a DSML for the software design back-translation that translates results and counterexamples of CPS, using the model checker U PPAAL. As a key benefit, back to the DSML. Part (iii) is highly important. Otherwise, our approach is able to translate counterexamples back to the the domain expert has to learn the model checker’s output domain-specific level even in case of large differences between format as well as the complete forward translation in order to DSML and the model checker’s input language. We show the correctness of our approach using a case study from the area of relate the counterexample to the DSML model. car-2-car communication. At present, there exists no concept for applying DSMC to CPS. On the one hand, existing concepts towards model I. I NTRODUCTION checking for CPS do not translate counterexamples back to the The software development for cyber-physical systems (CPS) DSML, e.g., COMDES-II [4], RT-DEVS [5], HUGO/RT [6], like (autonomous) cars, production machines, or rescue robots and a previous publication of our research group [7]. More- needs to undergo rigorous quality assurance measures. The over, the existing approaches do not support all CPS-relevant reason is that CPS do not work in isolation, but heavily interact domain aspects, as for example message delay (with lower and with each other and their environment, e.g., with humans. upper bounds), message loss, and buffer overflow avoidance Thus, CPS operate in a safety-critical context under hard real- strategies. On the other hand, DSMC concepts including a time constraints. Especially the functional correctness is of back-translation exist as well [8], [9], [10], but they only vital importance for CPS because (software) errors can lead address simple application scenarios with small language to life-threatening accidents. differences between DSML and the model checker’s input lan- Formal verification techniques such as model checking [1] guage. Such simple scenarios give rise to a forward translation are able to guarantee functional properties of the software (e.g., that consist of a single model-to-model (M2M) transformation deadlock freedom) and can provide counterexamples if a prop- step1 . A common approach to overcome larger language erty is violated. Counterexamples support the identification of differences is to split up the translation into a chain of multiple the root cause which is essential for correcting the software. steps [11]. The problem using such an approach is that a multi- However, the application of model checking to software step forward translation significantly complicates the back- development in practice is hindered by several factors [2]. translation of counterexamples, because it needs to overcome a A factor that we address in this paper is the rising software cascade of model transformations performed during the multi- complexity of CPS. In order to handle the complexity, such step forward translation. In addition, the back-translation needs systems are often developed by domain experts that use a to be adapted to each modification of the forward translation, domain-specific modeling language (DSML). However, these leading to a high amount of manual work. experts often have no experience with existing model checking In this paper, we present an approach to apply DSMC to the tools. Compared to a model checker, DSMLs provide high- software design for CPS. We present a successful realization level modeling constructs, e.g., hierarchical state machines, as well as domain-specific language concepts, e.g., for the 1 In the following, we use the term step to denote a single model-to-model exchange of asynchronous messages. Therefore, a DSML transformation. of DSMC including a multi-step forward translation between M ECHATRONICUML (MUML, [12]) as a high-level DSML for the software design of CPS, and the U PPAAL model Overtaker Overtakee checker [13]. Despite this multi-step forward translation, our approach allows to translate the counterexamples back to the DSML in one straightforward step, whereas the implemen- tation of this back-translation is independent of the number Fig. 1. Coordinated Overtaking of Two Cars of forward translation steps. We realize this by utilizing the model-to-model (M2M) traceability links of the forward translation, recorded by the model transformation engine. We evaluate our approach based on an example from the automotive domain. In particular, we show that our approach safety of the CPS. However, the software of a CPS typically enables a correct translation and back-translation between consists of a multitude of concurrently executed components. MUML and U PPAAL. Moreover, we demonstrate that our As a result, applying formal methods like model checking [16] approach provides helpful MUML counterexamples. becomes quickly impossible due to the state explosion prob- In summary, the contribution of this paper is as follows: (i) lem. A second obstacle is that the correctness of software We define and evaluate a DSMC for MUML using the model components may depend on the physical environment of the checker U PPAAL. (ii) We provide a transformation concept CPS. This applies, in particular, to the feedback controllers of that enables a multi-step forward translation but only requires the system that control the movement of (parts of) a CPS a single-step backward translation. like, e.g., the speed controller of the cars in Fig. 1. For Our paper is structured as follows: Section II summarizes such components, we are facing a so-called hybrid model the concept of MUML for verifying CPS based on a compo- checking problem [17] that is not solvable for realistic models sitional verification approach. In particular, it shows the key using current techniques [18]. MUML strives for the best role of DSMC in the context of this approach. In Section III, possible compromise between efficient simulation and formal we explain our concept for complex DSMC scenarios by correctness proofs for the software of a CPS. The resulting utilizing M2M traceability. Based on our concept, we explain approach is twofold. First, we tackle the state-explosion prob- our realization of the DSMC between MUML and U PPAAL in lem by a compositional verification approach that we describe Section IV and evaluate it in Section V. Afterwards, we discuss in more detail below. Second, we avoid hybrid verification related work in Section VI, before concluding the paper in by distinguishing between discrete software components and Section VII. feedback controller components in the MUML component model [15]. For discrete software components, the developer II. F OUNDATIONS : T HE C OMPOSITIONAL V ERIFICATION specifies a state-based real-time behavior that is formally ver- A PPROACH OF M ECHATRONICUML ified based on the compositional verification approach. Since M ECHATRONICUML (MUML, [12], [14], [15]) is a DSML the correctness of feedback controller components depends on for specifying the discrete-event software of CPS at appli- the physical environment, the developer does not specify a cation level. Thereby, MUML particularly focuses on the behavior model in MUML, but in a control engineering tool specification of a component-based software architecture, the like MATLAB/Simulink or Dymola/Modelica. For verifying specification of self-adaptive behavior, and the application- and validating the correct integration of discrete software level communication protocols that are required to coordinate components and feedback controllers, the developer exports different systems. the verified discrete software components to the control engi- A typical example of a CPS that requires the aforemen- neering tool. Then, the developer can test the correctness of tioned features is the coordination of an overtaking maneuver the feedback controllers and their integration with the discrete involving two cars as illustrated in Fig. 1. In this example, software components based on simulation [19], [20]. we use car-to-car (C2C) communication to coordinate and thereby to improve the safety of an overtaking maneuver. In The core idea of MUML’s compositional verification ap- our example, the red car (the overtaker) overtakes the yellow proach [7], [12], which is illustrated in Fig. 2, is a syntac- car (the overtakee) while the overtakee guarantees that it will tic decomposition of the software architecture into discrete not accelerate while it is being overtaken. Obviously, this sce- software components and application-level communication nario is safety-critical because an error in the communication protocols that define the interaction of the components. In protocol can result in an unsafe overtaking maneuver, e.g., MUML, we refer to these protocols as Real-Time Coordination if the overtakee assumes that it is not being overtaken but Protocols (RTCPs). Each RTCP specifies the asynchronous the overtaker assumes the contrary. In addition, we need to message-based communication of two communicating partners consider certain timing properties for the message exchange, called roles, while the behavior of each role is defined by a e.g., for detecting lost messages based on timeouts. state-based real-time behavior. The RTCP for the coordinated A major aim of MUML is to provide formal analyses for overtaking includes the overtaker role and the overtakee role. guaranteeing correctness of the specified model and thereby Then, each port of a component (Car in our example) must 1. Verify Real-Time Coordination Protocol via Model Checking properties that have been verified for the RTCP. This step is Coordination Protocol |= φ1, …,φn necessary because the implementation of a role’s behavior by AG ( stateActive(overtaker.overtaking) implies a port typically requires adding data exchange with the other Real-Time stateActive(overtakee.noA ccelar atio n) ); φ1 (RTCP) ports of the component, adding component-specific functions, Overtaking and accessing shared variables inside the component. This step is covered in detail in [12]. overtaker overtakee buffer size: 5 dela y: 1 s buffer size: 5 In the third step, we need to verify that each component is free of deadlocks [22]. Such deadlocks may result from an in- correct interaction of the different ports inside the component. 2. Verify Refinement «refines » |= φ1, …,φn «refines » We may verify additional safety, liveness, and reachability Components properties referring to this interaction if necessary. red:Car :overtakerCar :overtakeeCar yellow:Car In summary, we only need to consider one RTCP or one component at a time. This significantly improves the scalabil- ity of the verification and enables the formal verification of 3. Verify each Component Separately via Model Checking the software of a CPS. (at least for Deadlock Freedom) III. U TILIZING M2M T RACEABILITY FOR DSMC Fig. 2. Overview of the Compositional Verification Approach This section presents a DSMC approach that is suitable for the domain of CPS as it supports complex scenarios with implement one role of an RTCP2 . As a result, the behavior larger differences between DSML and model checker. The of each port is defined by a state-based real-time behavior applicability of our approach is the topic of Section IV by as well. Then, the decomposition of the software architecture presenting our DSMC for MUML’s RTCPs using U PPAAL. enables the verification of the discrete software components We depict our approach in Fig. 3. Similar to already of a CPS in three steps. existing DSMC approaches [8], [9], [10], we apply model In the first step, we verify all RTCPs w.r.t. safety, liveness, transformation techniques [23]. However, in contrast to the and reachability properties using model checking [16]. There- aforementioned DSMC approaches, we ease the task to over- fore, the roles of the RTCP have to be specified independently come larger differences between the DSML and the input of the components’ ports that implement them. The RTCP language of the model checker by allowing a multi-step contains all relevant information for the communication, i.e., translation (cf. [11]) but still only require a single-step back- the exchanged messages, their timing, the size of the FIFO translation. We achieve this by utilizing the M2M traceability message buffers, and non-functional properties of the connec- links that interrelate the models generated during the forward tion (e.g., message delay). The properties to be verified are translation and therefore indicate the semantic correspondence specified in MTCTL (M ECHATRONICUML TCTL), which is between the input/output elements of each translation step. a domain-specific variant of TCTL [21]. MTCTL is highly In fact, transformation languages such as QVTo [24] have a integrated with the behavior model of MUML. In our example, built-in traceability mechanism. Therefore, they do not require we require —among others— that the overtakee may not additional development effort in order to obtain these links accelerate while the overtaker is still overtaking. Therefore, while executing M2M transformations. we define the property 1 in MTCTL as depicted at the top Our approach starts with Activity 1 by applying the M2M of Fig. 2. For performing the verification, the RTCP including translation from the design model given in terms of the DSML all MTCTL properties needs to be translated to the model into the verification model that is based on the input language checker U PPAAL [13]. This translation is very complex as of the model checker. This translation may consist of multiple MUML defines several domain-specific aspects that U PPAAL steps, e.g., our translation of RTCPs to the input language does not provide, e.g., messages with parameters and time- of the U PPAAL model checker consists of 13 steps. In each consuming actions. Moreover, counterexamples of the model- forward translation step, the aforementioned traceability links checker must be translated back to the level of MUML in are automatically generated as an additional output. order to analyze them. The realization of both translations Activities 2-4 use state-of-the-art concepts: since existing (forward and backward) in the form of a domain-specific model checkers usually operate on a textual input language, model checking (DSMC) is the core contribution of this paper, Activity 2 includes a model-to-text transformation of the as the existing work does not provide concepts for such verification model. For example, U PPAAL requires a serial- complex scenarios. ization into an XML-based file format. Afterwards, the actual In the second step, we need to ensure that the ports of model checking takes place in Activity 3. Counterexamples the components correctly refine the roles of the RTCPs, i.e., generated during model checking are usually given in terms of the implementation of the port does not violate any of the a textual format as well. Therefore, Activity 4 includes a text- 2 In our example, we only provide one RTCP. However, in a fully realistic to-model transformation. The resulting counterexample model example, more RTCPs are necessary, e.g., for specifying the communications is a sequence of snapshots. Each snapshot provides a runtime within a car and between cars and infrastructure. view of the verification model. Therefore, as depicted in Fig. 3, Two-Step Forward Translation Legend Design Level Verification Level Design Model Intermediate Model Verification Model 1. Multi-Step Translation Verification Model State Transition Design Model (Model-to-Model) Step 1 ... Step n 2. Model-to-Text Runtime Snapshot cross-references cross-references Textual Verification Input Bidirectional Traceability Link 3. Automatic Verification Traceability Links ... ... ... ... Cross-Reference Textual Verification Counterexample Single-Step Counterexample e.g., to Indicate Results + Textual Model Back-Translation Model Active States Counterexamples 4. Text-to-Model Fig. 4. Resolving of Traceability Paths 5. Single-Step Verification Results + Verification Results and Back-Translation Counterexample Model Counterexample Model (Model-to-Model) Legend: checker snapshot in red, which marks two states as active (one Activity Artifact Data Flow Reference per state machine). In order to translate such a snapshot back to the DSML, the back-translation analyzes the traceability links Fig. 3. Utilizing M2M Traceability for DSMC generated in Activity 1. For example, for the two states marked active, it resolves the traceability path in the opposite direction, the parsed counterexample model includes cross-references until the states contained by the original design model are to the verification model. In our example application, these reached. These states are semantically equivalent to the states cross-references indicate which states of the U PPAAL timed marked active by the snapshot. In our example, the paths automata are active in each particular snapshot. consist of two traceability links. However, we do not need two separate back-translations steps. Instead, we use a generic The back-translation in Activity 5 receives the counterex- implementation of the back-translation that is independent of ample model and translates it back to the DSML level. the number of traceability links that form the path. We realize During the back-translation, all cross-references to elements it by resolving the traceability links incrementally until we of the verification model need to be replaced by corresponding reach an element of the design model. Thus, one single back- cross-references to design model elements. To resolve this translation step is sufficient to resolve traceability paths of semantic correspondence, the back-translation also receives the arbitrary length. traceability links generated during Activity 1 as an input. Since related approaches address only single-step translations [8], In our example, for the snapshot depicted in red, the [9], [10], they are restricted to direct traceability links between traceability paths indicate that both active states inside the design model and verification model. In contrast, our approach verification model evolved from one and the same state considers paths of traceability links with an arbitrary length, inside the design model. Thus, the back-translation generates which traverse the intermediate models generated during a a DSML snapshot that includes a cross-reference to mark multi-step translation. this state active. The back-translation can therefore provide A particular benefit of our approach is that the back- a DSML-specific runtime view of the original design model. translation does not depend on any conceptual or implemen- Our approach is limited to 1:n traceability links between tation details of the prior forward translation. It only depends two models. Thus, every step may translate an input element on the meta models of the DSML and the model checker. to more than one output element. In order to avoid ambiguous Therefore our approach is independent of the concrete number resolving results, it must not be the case that two or more input of forward translation steps, i.e., it enables an easy integration elements are translated to the same output element. However, of additional steps without changing the back-translation. the translation from a DSML to the input language of a model Fig. 4 illustrates the analysis of traceability paths in the checker is usually a refinement, i.e., it increases the number context of a forward translation consisting of two steps. In this of model elements (cf. Fig. 4). Therefore, this aspect does not example, a state machine inside the design model (consisting impose any practical restrictions. of two states) is translated to a verification model with two IV. DSMC FOR MUML’ S RTCP S USING U PPAAL parallel state machines, and an overall amount of five states. The traceability links (depicted in blue) connect corresponding In this section, we illustrate our DSMC between MUML’s elements inside the design model, the intermediate model, and RTCPs and the model checker U PPAAL. At first, we briefly in- the verification model. The model checker’s counterexample troduce U PPAAL (cf. Section IV-A). Then, in Section IV-B, we model (depicted in the bottom right corner of Fig. 4) uses explain MUML’s Real-Time Coordination Protocols (RTCPs) cross-references to indicate which states of the two state as well as our overtaking scenario in more detail. Afterwards, machines inside the verification model are active during each we present our DSMC: We show the model-to-model trans- snapshot. For example, Fig. 4 highlights a single model lation from RTCPs to U PPAAL in Section IV-C. Then, we explain the automated invocation of U PPAAL in Section IV-D. B. RTCPs and the Overtaking Example Finally, we explain the model-to-model back-translation of counterexamples from U PPAAL to RTCPs in Section IV-E. In the following, we explain RTCPs in detail using the We rely on the QVTo language [24] for all model-to-model RTCP Overtaking, which we introduced in Section II. As we transformations to utilize its traceability links in the back- already stated before, its task is to specify a coordination translation. Our implementation and our examples are open between two cars by exchanging asynchronous messages under source and available for download on our website [25]. hard real-time constraints to enable a safe overtaking. Fig. 5 shows the RTCP Overtaking with its two roles overtaker and A. The Model Checker U PPAAL overtakee. As illustrated, each role of the RTCP may store five messages within its incoming message buffer received from U PPAAL [13] is a tool for modeling and model checking the other role. The transmission delay (depicted at the role real-time systems (such as CPS) based on networks of timed connector) for a message is 1 s. automata [26]. U PPAAL timed automata are state machines that consist of states, transitions, variables, and real-valued clocks3 . The state-based real-time behavior of each role is specified A clock measures the progress of time in a system. Time may by a Real-Time Statechart (RTSC). RTSCs are a combination only pass in states and not while firing a transition. Based of timed automata and UML state machines [28]. Like timed on its clocks, a timed automaton enables to specify time- automata, RTSCs may define clocks for expressing time con- dependent behavior using time guards, resets, and invariants. A straints. Similar to UML but in contrast to U PPAAL’s timed time guard is a boolean constraint that is part of the enabling automata, RTSCs enable to use, among others, (i) hierarchical condition of a transition. A transition may only fire if the compositions of states (including entry- and exit-points), (ii) current clock values fulfill the time guard. Resets set a clock entry- and exit-actions for states, (iii) composite transitions (a back to zero. An invariant is a boolean constraint on a state transition where the source or target is a hierarchical state), that must be fulfilled as long as the state is active. (iv) time-consuming transitions, and (v) asynchronous com- Timed automata are flat, i.e., they do not contain hierarchical munication at transitions, i.e., consuming a received message states. Moreover, they may be composed to networks of timed from a buffer, or sending a message to the other role. automata that communicate in a synchronous fashion using so- The lower part of Fig. 5 shows the RTSCs for both roles of called channels [27]. However —as a major drawback— U P - the RTCP Overtaking. A “/” separates a transition’s enabling PAAL does not provide modeling elements for the domain of conditions (a guard, a message to be received, and/or a clock CPS like asynchronous message-based communication (incl. constraint) from its effect (a sent message, a clock reset, message parameters) and time-consuming transitions. and/or an action). The general behavior of the RTCP is as U PPAAL can verify a subset of the timed computation tree follows: First, the overtaker requests to overtake the overtakee logic (TCTL, [21]), referred to as UTCTL in this paper. In by sending a request. At the same time, the overtaker resets particular, it supports three kinds of properties: reachability the clock c when entering the requested state and awaits a (something may happen), safety (“something bad will never response within six seconds as the state invariant is c  6 s. happen” [27, p.8]), and liveness (“something will eventu- The overtakee replies by either an accept or decline message. ally happen” [27, p.9]). When verifying a property, U PPAAL If the overtakee accepts the request, it must drive with a generates the textual result (i.e., whether the property is constant speed (accelerating and braking are forbidden) to fulfilled). Moreover, U PPAAL can —if available— generate avoid a collision with the overtaker that will drive close to textual traces. A trace is an execution path of the network the overtakee before it starts to overtake. When receiving of timed automata represented by a sequence of snapshots4 . the accept message, the overtaker switches to overtaking.init Each snapshot contains the active state of all timed automata and may accelerate. The transition between overtaking.init and in the network and the values of all clocks and variables. A overtaking.changed is time-consuming as it has a deadline of snapshot change occurs for three reasons: (i) time passes, (ii) a exactly 5 s. Thus, the overtaker has five seconds to change timed automaton fires a transition, or (iii) two timed automata the lane and start the overtaking (for simplicity reasons, we synchronize using a common channel and synchronously fire assume that this is always possible). After exactly five seconds, their transitions. the overtaker announces that it has changed the lane by sending In particular, U PPAAL can produce a textual trace (1) if a a laneChanged message. From then on, the overtakee may reachability property is fulfilled or (2) if a safety or liveness brake, but may still not accelerate until a finish message property fails. In case (1), the trace leads to a snapshot where announces that the overtaking has been carried out. Due to the property is fulfilled. In case (2), the trace leads to a the invariant of state overtaking, the overtaker has to send snapshot where the property is violated. Therefore, a trace message finish at most ten seconds after the overtaking has of case (2) is also called a counterexample. started (again, for simplicity reasons we assume that this is always possible). 3 In this paper, we use the terms states and transitions instead of U PPAAL ’s The behavior specified by a RTCP is typically safety- terminology of locations and edges to improve the understandability of our critical. For example, an error in the RTCP Overtaking DSMC between MUML and U PPAAL. 4 In U PPAAL , snapshots are referred to as states. We use the term snapshot may lead to an accident if the overtakee car accelerates to avoid confusion with states of a RTSC (cf. Section IV-B). even though the overtaking is still ongoing. Therefore, we 1. AG not deadlock 2. AG not bufferOverflow Overtaking 3. AG (stateActive(overtaker.overtaking) implies overtaker overtakee stateActive(overtakee.noAcceleration)) buffer buffer 4. forall(s:States) EF stateActive(s) size: 5 delay: 1s size: 5 overtaker clock c overtakee noOvertaking overtaking noOvertaking noAcceleration invariant c 10s clock c2 / request requested accept / / accept entry / {reset: c} noBraking invariant c 6s received init request / [c 6s] entry / {reset: c} invariant c2 3s request / / laneChanged laneChanged / init changed init entry / {reset: c2} decline / deadline: 5s / decline finish / brakingAllowed / finish Legend RTCP Role Role Connector RTSC State Urgent Transition Non-Urgent Transition Entry Point Exit Point Fig. 5. MUML Real-Time Coordination Protocol Overtaking Initial After Deadline After Hierarchy After UPPAAL in Fig. 6 (we provide detailed information about all 13 steps in Model Normalization Normalization Migration [c_active] A ... Ex ... D our technical report [29]). The first two steps that we illustrate A A A Ex D C are normalizations on the MUML level, i.e., they reduce the ch! B B Idle B number of different modeling constructs. We do this in order {reset: c} ... to simplify the final step: the migration to U PPAAL. deadline: /m {reset: c} 2-3s BC B BC ... BC c 3s c 3s send(m), The first step normalizes deadlines by means of dedi- C ... ... [c 2s] /m [c 2s] / m ... cated intermediate states, emulating the execution of time- Idle C {c_active :=true} Connector C consuming transitions. In our example in Fig. 6, the deadline ch? / ... ... of the time-consuming transition from state B to C is replaced D {c_active D :=false} C ... ... by a new clock c, the intermediate state BC (including an invariant) and two additional transitions. The invariant of state BC defines how long the intermediate state may be active. Fig. 6. Multi-Step Translation from MUML to U PPAAL The clock constraint below defines when the transition to state C may fire. The recorded traceability links between the need (domain-specific) model checking of RTCPs using U P - respective elements are depicted by blue dashed arrows. Our PAAL. As a prerequisite, we specify properties of the RTCP translation is a 1:n refinement, because each design model to be verified using our textual formal language MTCTL element is translated to one or more output elements. (M ECHATRONICUML TCTL). Another normalization applies a flattening concept, which The RTCP Overtaking defines four MTCTL properties: three is based on the work of David and Möller [30], transforming safety and one reachability property (cf. Fig. 5). The first hierarchical RTSCs into flat ones. As a consequence, this trans- property states that the model contains no deadlock, while lation splits the hierarchical RTSC into several flat RTSCs. the second ensures that the message buffers never overflow. Moreover, it replaces state entry- and exit-points, adds idle The third property states that whenever the overtaker is in states (if a region may become inactive), and adds channels state overtaking, the overtakee must be in state noAccelaration. and global variables for synchronizing the behavior of different Thus, it enforces the aforementioned requirement that the RTSCs (the variables indicate if a set of states is active, which overtakee must not accelerate whenever the overtaking is in allows exiting a hierarchy level). In our example, the results progress. The fourth property specifies that all states of the are two flat RTSCs. Moreover, we add an idle state to the protocol are reachable. In the remainder of this section, we lower RTSC, replace the exit-point by state Ex, and add one present our DSMC for MUML’s RTCPs using U PPAAL. channel ch as well as one variable c active. Finally, our migration step replaces all remaining domain C. Model-To-Model Translation from RTCPs to U PPAAL concepts, e.g., the asynchronous message exchange. Similar According to Activity 1 of our concept (cf. Fig. 3), we to Knapp et al. [6], we generate additional timed automata to developed the model-to-model translation from RTCPs (in- encode the transmission connector (including properties such cluding the MTCTL properties) to U PPAAL timed automata as message loss and delay) and the buffering of messages (in- (including UTCTL properties). Due to the huge differences cluding buffer overflow avoidance strategies). In our example, between RTCPs and U PPAAL, we separated our translation we have to transform the sending of message m when firing into 13 steps, each one addressing a particular concern of the the transition from state BC to C into an U PPAAL function, and RTCP and/or the MTCTL properties. have to generate a connector such that the message can be sent. Due to the limited size of this paper, we briefly explain Moreover, we translate states, transitions, clocks, variables, three of these steps on a simplified example, which we depict and channels of MUML into their U PPAAL representation. In summary, the translation shown in Fig. 6 is a refinement (counterexample) trace in one single step, despite the 13 steps from one hierarchical RTSC to an U PPAAL model consisting from MUML to U PPAAL. In particular, our back-translation of three timed automata and several hundred lines of code. All is very small as it needs only 609 QVTo LOCs, compared translation steps record bidirectional traceability links between to 9,239 LOCs for the translation from MUML to U PPAAL semantically corresponding elements. For example, a bidi- (ca. 7%). Moreover, the implementation was straighforward rectional traceability path exists between the time-consuming as we only had to define to which kind of MUML element a transition from state B to C and the U PPAAL state BC. particular U PPAAL element needs to be transformed. Presently, Beside the above translation of the RTSCs, we also translate (counterexample) traces are printed as SVG files. the specified MTCTL properties to UTCTL. For example, the last property depicted in Fig. 5 (expressing that all states must V. C ASE S TUDY be reachable) corresponds to twelve UTCTL properties, one We conduct a case study based on the guidelines by for each state of the RTSCs because UTCTL does not support Kitchenham et al. [31] for evaluating our approach. quantification over all states. A. Case Study Context D. Automated Invocation of U PPAAL The objective of our case study is evaluating if our DSMC Next, we implemented the Activities 2-4 (cf. Fig. 3) of our for MUML’s RTCPs using the U PPAAL model checker (which approach. In particular, we carried out Activity 2 by means is based on our general DSMC approach) is correct and if it of a model-to-text transformation using Xtend5 , generating provides helpful counterexamples at the level of MUML. U PPAAL’s XML-based input format for timed automata and We conduct our case study using 14 existing RTCPs of the textual UTCTL properties. For Activity 3, we invoke different interconnected transportation systems (e.g., cars, rail- U PPAAL’s command line verifier and obtain textual results ways, robots). These RTCPs focus on various use cases for and —if available— textual traces (e.g., a counterexample). coordination, such as collision avoidance or our overtaking As defined for Activity 4, we need to parse the textual scenario. Within the paper, we show the evaluation of the (counterexample) trace into a model. Therefore, we defined RTCP Overtaking introduced in Section IV-B. The evaluation a meta model for U PPAAL traces and developed a text-to- of all other RTCPs is provided on our website [25]. model transformation using Xtext6 . The parsed trace model in- cludes cross-references to the U PPAAL timed automata model. B. Setting the Hypothesis Among others, it reflects which states are active inside a We only consider RTCPs that are —according to our particular snapshot and which values are assigned to clocks. expertise— initially correct w.r.t. their MTCTL properties. E. Model-To-Model Back-Translation from U PPAAL to RTCPs Then, we deliberately introduce errors in order force U PPAAL to produce counterexamples for defined safety or liveness As a basis for the model-to-model back-translation of traces properties expressed in MTCTL. (Activity 5 in Fig. 3), we defined a meta model for MUML Our case study has three evaluation hypotheses: (H1) traces as the target for our back-translation. Structurally, this Our DSMC approach correctly translates all RTCPs (incl. meta model is similar to the (counterexample) trace meta all MTCTL properties) to U PPAAL. (H2) Our DSMC ap- model for U PPAAL, i.e., it provides means to model a sequence proach correctly translates all U PPAAL counterexamples back of snapshots (depicted in the middle of Fig. 7). However, these to MUML. (H3) The MUML counterexamples help domain snapshots provide specific information of the original MUML experts to detect the root cause of property violations. design model at runtime, i.e., a MUML snapshot describes the For evaluating hypothesis H1, we manually translate RTCPs active states and transitions inside RTSCs, the current values that are correct w.r.t. their MTCTL properties to U PPAAL and of variables and clocks, the contents of the message buffers, compare them with the outputs of our automatic translation. and which messages are currently in transit. Both should be equivalent. We evaluate hypothesis H2 similar Afterwards, we implemented a model-to-model transfor- to H1. Thus, we manually translate U PPAAL counterexamples mation that translates U PPAAL snapshots back to MUML back to MUML and compare them with the counterexamples (see [29] for details of the implementation concept). Among that are back-translated automatically. Both sets should be others, we translate active U PPAAL states back to the corre- equivalent as well. In addition, our DSMC should be able sponding active RTSC states or transitions. In order to traverse to provide a counterexample at the level of MUML for each all the 13 forward translation steps inside a single back- U PPAAL counterexample. The MUML counterexample should translation step, we resolve traceability links incrementally only refer to elements of the original MUML design model. until we reach a MUML element (e.g., an RTSC state) that is Concerning the evaluation of H3, we give the incorrect RTCP part of the original RTCP. We carry out the resolving by means and the MUML counterexample to a domain expert that of QVTo’s invresolve operation [24], i.e., we utilize traceability already has 1.5 years of experience in MUML. However, our links recorded automatically during the forward translation. As domain expert has no knowledge of U PPAAL and does not a result, we implemented the back-translation of the complete know the root cause of the errors. We consider H3 as fulfilled, 5 https://eclipse.org/xtend/ if the counterexample facilitates finding the root cause of the 6 https://eclipse.org/Xtext/ error for the domain expert. Role overtaker overtaker clock c1=1s overtaker. overtaker. overtaker overtaking noOvertaking noOvertaking overtaking Incoming invariant c ≤ 10s Message Buffer: ... entry / {reset: c} Trace Trace Empty Snapshot 1 Snapshot 1 c c c ... ... overtaker2 overtakee2 decline / init ... overtakee overtaker c c Connector: No Message in Transit + 381 LOC in ... ... UPPAAL Role overtakee overtakee Incoming Trace Trace Message Buffer: noOvertaking / accept noAcceleration c c c Empty Snapshot n Snapshot n finish / ... ... request / AG (stateActive(overtaker.overtaking) implies overtakee. overtakee. stateActive(overtakee.noAcceleration)) noOvertaking overtakee noAcceleration Fig. 7. Back-Translation of an U PPAAL Counterexample Trace to MUML C. Preparing the Input Models translated back, the corresponding counterexamples match First, we manually assure that all 14 RTCPs are correct w.r.t. semantically, and the MUML counterexamples only refer to their MTCTL properties according to the MUML semantics. the original RTCPs. For example, our DSMC returned a Then, we manually create the 14 U PPAAL models. Next, valid counterexample when verifying the incorrect version we systematically introduce one modeling error into each of RTCP Overtaking with Property 3. Fig. 7 illustrates the RTCP. These errors include missing transitions, missing sent counterexamples of U PPAAL and MUML for this property. or received messages, inappropriate message delays, or false In particular, the figure sketches the last snapshot of the timeout periods. For each error, we define a reachability counterexample for both languages. The correspondence (i.e., or safety property that is meant to reveal the error such the traceability paths) between the modeling elements is that we get a counterexample for each RTCP. Finally, we highlighted using purple dashed arrows. Concerning the last manually create all 14 MUML counterexamples. For example, MUML snapshot, the state overtaking.init and the transition to produce a counterexample for the Overtaking RTCP, we from noAcceleration to noOvertaking are active which violates insert an error to the RTSC of role overtaker (cf. Fig. 5). Property 3. Moreover, the snapshot shows that the incoming This RTSC encodes a response timeout using the invariant in message buffers are empty, no message is in transit, and that state noOvertaking.requested and the transition leading from clock overtaker.c1 is at 1s. this state to noOvertaking.init. If this transition is fired, the Our domain expert was able to detect the root cause for overtaker assumes that the message was lost and, therefore, every property violation based on the erroneous RTCP and the that the overtakee will not answer. We reduce the invariant of back-translated counterexample. Moreover, he stated that the state noOvertaking.requested as well as the clock constraint of back-translated counterexamples supported him in solving the the transition that leads to state noOvertaking.init from 6 s to problem (especially for complex protocols like Overtaking). 4 s. This change violates the safety property 3, i.e., overtakee For example, the domain expert was able to detect that the may accelerate during the overtaking. The reason for this is as reduced timeout period in state overtaker.noOvertaking causes follows: If the overtaker is in state noOvertaking.requested, it the violation depicted in Fig. 7. The counterexample correctly can return to state noOvertaking.init although the overtakee has shows that overtakee accepts the overtaking, but overtaker switched to state noAcceleration and has sent an acceptance switches back to noOvertaking.init before the accept message message that did not arrive yet. Then, the overtaker may arrives due to the reduced invariant of c  4 s. This problem change to state overtaking by sending a new request and enables overtaker to send a second request message. This consuming the accept message for the old request. Then, the causes overtakee to switch from noAcceleration to noOver- overtakee will receive the new request message, which forces taking, which violates the property. it to change back to the state noOvertaking. E. Analyzing the Results D. Validating the Hypotheses Our case study demonstrates that our DSMC correctly For every correct RTCP, we execute our DSMC with all translates from MUML to U PPAAL, and U PPAAL counterex- available MTCTL properties (including the one that is meant amples back to MUML. Hence, we consider our first and to indicate the error). As a result, we get valid U PPAAL models second evaluation hypotheses as fulfilled. The back-translated that correspond to our manually created ones. U PPAAL reports counterexamples allowed to identify the root cause of all that they fulfill all defined MTCTL properties. property violations. Hence, we consider our third evaluation For every erroneous RTCP, we execute our DSMC with hypothesis as fulfilled as well. the MTCTL property that is meant to indicate the error. As In our case study, the most important threats to validity are a result, we obtain valid MUML counterexamples for all as follows: (1) We might have made mistakes in our manual RTCPs, i.e., the U PPAAL counterexamples were successfully translations (forward and backward) and when comparing the results. Thus, the translations might be in fact incorrect. (2) We of multi-step translations, enriching a model transformation only considered 14 RTCPs and introduced only one error in manually implies a huge development effort. In contrast, each RTCP. Even though we consider this example as realistic, our approach demonstrates that traceability links generated other realistic protocols, properties, and errors could exist that implicitly by the transformation engine are sufficient even in are not correctly translated. (3) It might be an exception that case of multi-step translations. our domain expert found all errors. Other domain experts Combemale et al. [39] provide a generic approach for the could be less successful. Moreover, the errors might have back-translation of execution traces such as counterexamples, been too easy to identify. (4) We cannot precisely state how but require a formal definition of the operational DSML much influence our back-translated counterexamples had on semantics. Hegedüs et al. [40] apply traceability links for our domain expert for finding the errors. the back-translation, but require the operational semantics of the DSML and the verification formalism (e.g., a model VI. R ELATED W ORK checker input language) to be formalized in terms of graph Several concepts towards model checking of CPS exist, transformations. Thus, in contrast to our approach, both require which support a translation from a DSML towards a model a formalization of the operational DSML semantics. However, checker, e.g., COMDES-II [4], RT-DEVS [5], Dragomir et DSMLs such as MUML are often equipped with informal al. [32], AADL [33], Tiwari et al. [34], HUGO/RT [6], and the semantics, such that a complete formal semantics definition Compositional Interchange Format (CIF) [35]. However, they at DSML level represents an additional burden. all do not provide concepts for back-translating counterexam- ples. In the scope of this paper, we rather discuss related work VII. C ONCLUSION AND F UTURE W ORK that fully hides formal methods by providing a back-translation In this paper, we provide a DSMC in the context of CPS for counterexamples. We restrict ourselves to approaches that between MUML’s RTCPs and the model checker U PPAAL. establish a close link between counterexamples and design In contrast to related work that supports model checking of model, creating explicit cross-references. An extended discus- CPS, we enable the back-translation of counterexamples and sion of related work may be found in our technical report [29]. support the relevant aspects of CPS-specific communication Molotnikov et al. [36] address the verification of domain- protocols at application level. We realize this DSMC using a specific extensions to the C programming language. The new concept that enables the usage of multi-step forward trans- verification is achieved by a multi-step translation to a basic lations but still only needs a single-step back-translation. In our form of verifiable C. By utilizing traceability information, the general DSMC concept, we propose to utilize the traceability verification results are translated back to the domain-specific links of the forward translation that are automatically provided level. In contrast to our approach, a conceptual consideration by the model transformation engine. These links enable us to of the back-translation is not in the scope of their paper. identify the corresponding model elements between the design Guerra et al. [8] present the BaVeL DSML for the mod- and the verification model, independently of the concrete eling of DSMC workflows including back-translations. The implementation of the forward translation. In a case study, language uses triple graphs [37] for the specification of we showed that our DSMC between MUML’s RTCPs and translation rules. During the forward translation, these rules U PPAAL enables a correct translation and back-translation, and produce the required traceability links that are later used by the that it is able to provide helpful counterexamples. back-translation. However, in case of multi-step translations, Transformation developers should benefit from our approach the approach requires a multi-step back-translation as well, when implementing new DSMC solutions, as they can split up because each step of the forward translation must be traced the translation into multiple steps and only need few LOCs back individually by means of a separate triple graph. In for the implementation of the back-translation. These benefits contrast, our approach enables a single-step back-translation should reduce their development time and should lead to a that is independent of the number of forward translation steps. maintainable solution. Authors of related approaches can use Zalila et al. [38] provide a methodology for DSMC that is our complex application scenario to evaluate their work, since based on a metamodeling pattern for executable DSMLs. Shah our implementation is open source [25] and the specifications et al. [10] present a translation of structural UML models to of MUML [15] and U PPAAL [13] are publicly available. Alloy for static consistency analysis. The authors use a meta Future work will further evaluate our general approach transformation to generate the actual back-translation on-the- on other complex applications scenarios. Moreover, we will fly from the recorded traceability links. The MADES approach further evaluate our DSMC between MUML and U PPAAL in by Baresi et al. [9] uses traceability only to highlight the order to find out if our approach reduces the maintainability correspondences between counterexample elements and the in comparison to related work. equivalent elements of the design model (without providing a proper back-translation). Common to these three approaches is ACKNOWLEDGMENTS that they require an additional instrumentation of the forward translation to produce a specific kind of traceability output. We thank Marie C. Platenius and Jörg Holtmann for feed- Thus, transformation developers need to enrich the basic back on drafts of the paper, and Goran Piskachev for his help translation with additional traceability logic. Especially in case in our case study. Christopher Gerking is member of the PhD program “Design of Flexible Work Environments — Human- [19] C. Heinzemann, J. Rieke, and W. Schäfer, “Simulating self-adaptive Centric Use of Cyber-Physical Systems in Industry 4.0”, component-based systems using MATLAB/Simulink,” in Proc. 2013 IEEE 7th International Conference on Self-Adaptive and Self-Organizing supported by the federal state of North Rhine-Westphalia. Systems. IEEE, 2013, pp. 71–80. [20] U. Pohlmann, J. Holtmann, M. Meyer, and C. Gerking, “Generating R EFERENCES Modelica models from software specifications for the simulation of cyber-physical systems,” in Proc. 2014 40th EUROMICRO Conference [1] E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. MIT on Software Engineering and Advanced Applications. IEEE, 2014, pp. Press, 2000. 191–198. [2] J. A. Davis, M. Clark, D. D. Cofer, A. Fifarek, J. Hinchman, J. Hoffman, [21] R. Alur, C. Courcoubetis, and D. L. Dill, “Model-checking in dense real- B. Hulbert, S. P. Miller, and L. Wagner, “Study on the barriers to the time,” Information and Computation, vol. 104, no. 1, pp. 2–34, 1993. industrial adoption of formal methods,” in Formal Methods for Industrial [22] H. Giese, “A formal calculus for the compositional pattern-based design Critical Systems, ser. LNCS, C. Pecheur and M. Dierkes, Eds., vol. 8187. of correct real-time systems,” Software Engineering Group, University Springer, 2013, pp. 63–77. of Paderborn, Tech. Rep. tr-ri-03-240, Jul. 2003. [3] W. Visser, M. B. Dwyer, and M. W. Whalen, “The hidden models of [23] S. Sendall and W. Kozaczynski, “Model transformation: The heart and model checking,” Software & Systems Modeling, vol. 11, no. 4, pp. soul of model-driven software development,” IEEE Softw., vol. 20, no. 5, 541–555, 2012. pp. 42–45, 2003. [4] X. Ke, P. Pettersson, K. Sierszecki, and C. Angelov, “Verification of [24] Object Management Group, MOF 2.0 Query/View/Transformation Spec- COMDES-II systems using U PPAAL with model transformation,” in ification, Feb. 2015, no. formal/15-02-01. Proc. 14th IEEE International Conference on Embedded and Real-Time [25] [Online]. Available: https://trac.cs.upb.de/mechatronicuml/wiki/ Computing Systems and Applications. IEEE, 2008, pp. 153–160. PaperModevva2015 [5] A. Furfaro and L. Nigro, “Embedded control systems design based [26] J. Bengtsson and W. Yi, “Timed automata,” in Lectures on Concurrency on RT-DEVS and temporal analysis using U PPAAL,” in Proc. of the and Petri Nets, ser. LNCS, J. Desel, W. Reisig, and G. Rozenberg, Eds. International Multiconference on Computer Science and Information Springer, 2004, vol. 3098, pp. 87–124. Technology, M. Ganzha, M. Paprzycki, and T. Pełech-Pilichowski, Eds., [27] G. Behrmann, A. David, and K. G. Larsen, A Tutorial on U PPAAL 4.0, vol. 3. IEEE, 2008, pp. 601–608. Department of Computer Science, Aalborg University, Nov. 2006. [6] A. Knapp, S. Merz, and C. Rauh, “Model checking timed UML state [28] Object Management Group, OMG Unified Modeling Language, Mar. machines and collaborations,” in Formal Techniques in Real-Time and 2015, no. formal/15-03-01. Fault-Tolerant Systems, ser. LNCS, W. Damm and E.-R. Olderog, Eds., [29] S. Dziwok, C. Gerking, and C. Heinzemann, “Domain-specific model vol. 2469. Springer, 2002, pp. 395–416. checking of M ECHATRONICUML models using U PPAAL,” Software [7] H. Giese, M. Tichy, S. Burmester, W. Schäfer, and S. Flake, “Towards Engineering Group, Heinz Nixdorf Institute, University of Paderborn, the compositional verification of real-time UML designs,” in Proc. Tech. Rep. tr-ri-15-346, Jul. 2015. of the 11th ACM SIGSOFT Symposium on Foundations of Software [30] A. David, M. O. Möller, and W. Yi, “Formal verification of UML Engineering. ACM, 2003, pp. 38–47. statecharts with real-time extensions,” in Fundamental Approaches to [8] E. Guerra, J. de Lara, A. Malizia, and P. Dı́az, “Supporting user-oriented Software Engineering, ser. Lecture Notes in Computer Science, R.-D. analysis for multi-view domain-specific visual languages,” Information Kutsche and H. Weber, Eds., vol. 2306. Springer, 2002, pp. 218–232. and Software Technology, vol. 51, no. 4, pp. 769–784, 2009. [31] B. Kitchenham, L. Pickard, and S. L. Pfleeger, “Case studies for method [9] L. Baresi, G. Blohm, D. S. Kolovos, N. Matragkas, A. Motta, R. F. and tool evaluation,” IEEE Softw., vol. 12, no. 4, pp. 52–62, Jul. 1995. Paige, A. Radjenovic, and M. Rossi, “Formal verification and validation [32] I. Dragomir, I. Ober, and C. Percebois, “Contract-based modeling and of embedded systems: the UML-based MADES approach,” Software & verification of timed safety requirements within SysML,” Software & Systems Modeling, vol. 14, no. 1, pp. 343–363, Feb. 2015. Systems Modeling, Jul. 2015. [10] S. M. A. Shah, K. Anastasakis, and B. Bordbar, “From UML to [33] A. Johnsen, K. Lundqvist, P. Pettersson, and O. Jaradat, “Automated Alloy and back again,” in Models in Software Engineering, ser. LNCS, verification of AADL-specifications using U PPAAL,” in Proc. 2012 IEEE S. Ghosh, Ed., vol. 6002. Springer, 2010, pp. 158–171. 14th International Symposium on High-Assurance Systems Engineering. [11] A. Etien, V. Aranega, X. Blanc, and R. F. Paige, “Chaining model IEEE, 2012, pp. 130–138. transformations,” in Proc. of the First Workshop on the Analysis of Model [34] A. Tiwari, N. Shankar, and J. M. Rushby, “Invisible formal methods for Transformations. ACM, 2012, pp. 9–14. embedded control systems,” Proc. IEEE, vol. 91, no. 1, pp. 29–39, Jan. [12] C. Heinzemann, C. Brenner, S. Dziwok, and W. Schäfer, “Automata- 2003. based refinement checking for real-time systems,” Computer Science - [35] D. E. Nadales Agut, M. A. Reniers, R. R. Schiffelers, K. Y. Jörgensen, Research and Development, vol. 30, no. 3, pp. 255–283, Aug. 2015. and D. van Beek, “A semantic-preserving transformation from the [13] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi, compositional interchange format to U PPAAL,” in Proc. of the 18th IFAC “U PPAAL- a tool suite for automatic verification of real-time systems,” World Congress, S. Bittanti, A. Cenedese, and S. Zampieri, Eds., 2011, in Verification and Control, ser. LNCS, R. Alur, T. A. Henzinger, and pp. 12 496–12 502. E. D. Sontag, Eds., vol. 1066. Springer, 1996, pp. 232–243. [36] Z. Molotnikov, M. Völter, and D. Ratiu, “Automated domain-specific [14] S. Becker, S. Dziwok, C. Gerking, C. Heinzemann, W. Schäfer, C verification with mbeddr,” in Proc. of the 29th ACM/IEEE Inter- M. Meyer, and U. Pohlmann, “The M ECHATRONICUML method: national Conference on Automated Software Engineering, I. Crnkovic, Model-driven software engineering of self-adaptive mechatronic sys- M. Chechik, and P. Grünbacher, Eds. ACM, 2014, pp. 539–550. tems,” in Companion Proc. of the 36th International Conference on [37] A. Schürr, “Specification of graph translators with triple graph gram- Software Engineering. ACM, 2014, pp. 614–615. mars,” in Graph-Theoretic Concepts in Computer Science, ser. LNCS, [15] S. Becker, S. Dziwok, C. Gerking, C. Heinzemann, S. Thiele, E. W. Mayr, G. Schmidt, and G. Tinhofer, Eds., vol. 903. Springer, W. Schäfer, M. Meyer, U. Pohlmann, C. Priesterjahn, and M. Tichy, 1995, pp. 151–163. “The M ECHATRONICUML design method — process and language for [38] F. Zalila, X. Crégut, and M. Pantel, “Formal verification integration platform-independent modeling,” Software Engineering Group, Heinz approach for DSML,” in Model-Driven Engineering Languages and Nixdorf Institute, University of Paderborn, Tech. Rep. tr-ri-14-337, Mar. Systems, ser. LNCS, A. Moreira, B. Schätz, J. Gray, A. Vallecillo, and 2014. P. Clarke, Eds. Springer, 2013, vol. 8107, pp. 336–351. [16] C. Baier and J.-P. Katoen, Principles of Model Checking. MIT Press, [39] B. Combemale, L. Gonnord, and V. Rusu, “A generic tool for tracing 2008. executions back to a DSML’s operational semantics,” in Modelling [17] T. A. Henzinger, “The theory of hybrid automata,” in Proc. 11th Annual Foundations and Applications, ser. LNCS, R. B. France, J. M. Küster, IEEE Symposium on Logic in Computer Science. IEEE, Jul. 1996, pp. B. Bordbar, and R. F. Paige, Eds., vol. 6698. Springer, 2011, pp. 35–51. 278–292. [40] Á. Hegedüs, G. Bergmann, I. Ráth, and D. Varró, “Back-annotation of [18] A. Eggers, N. Ramdani, N. S. Nedialkov, and M. Fränzle, “Improving the simulation traces with change-driven model transformations,” in 2010 SAT modulo ODE approach to hybrid systems analysis by combining 8th IEEE International Conference on Software Engineering and Formal different enclosure methods,” Software & Systems Modeling, vol. 14, Methods, J. L. Fiadeiro, S. Gnesi, and A. Maggiolo-Schettini, Eds. no. 1, pp. 121–148, Feb. 2015. IEEE, 2010, pp. 145–155.