=Paper=
{{Paper
|id=Vol-1514/paper3
|storemode=property
|title=Domain-Specific Model Checking for Cyber-Physical Systems
|pdfUrl=https://ceur-ws.org/Vol-1514/paper3.pdf
|volume=Vol-1514
|dblpUrl=https://dblp.org/rec/conf/models/GerkingSDH15
}}
==Domain-Specific Model Checking for Cyber-Physical Systems==
https://ceur-ws.org/Vol-1514/paper3.pdf
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.