Back-annotation of Simulation Traces with Change-Driven Model Transformations
A´bel Hegedu¨s, Ga´bor Bergmann, Istva´n Ra´th and Da´niel Varro´
Department of Measurement and Information Systems
Budapest University of Technology and Economics
Budapest, Hungary
Email: fhegedusa,bergmann,rath,varrog@mit.bme.hu
Abstract—Model-driven analysis aims at detecting design
flaws early in high-level design models by automatically de-
riving mathematical models. These analysis models are sub-
sequently investigated by formal verification and validation
(V&V) tools, which may retrieve traces violating a certain
requirement. Back-annotation aims at mapping back the results
of V&V tools to the design model in order to highlight the real
source of the fault, to ease making necessary amendments.
Here we propose a technique for the back-annotation of sim-
ulation traces based on change-driven model transformations.
Simulation traces of analysis models will be persisted as a
change model with high-level change commands representing
macro steps of a trace. This trace is back-annotated to the
design model using change-driven transformation rules, which
bridge the conceptual differences between macro steps in the
analysis and design traces. Our concepts will be demonstrated
on the back-annotation problem for analyzing BPEL processes
using a Petri net simulator.
Keywords-back-annotation; simulation traces; change-driven
model transformations
This work was partially supported by EU projects
SENSORIA (IST-3-016004) and SecureChange (ICT-FET-
231101).
I. INTRODUCTION
Model-driven analysis with hidden formal methods has
become a popular approach in critical systems and services
design. Various approaches with close conceptual correspon-
dence has been proposed in various application domains
such as service-oriented computing [1], [2], dependable
systems [3]–[5], avionics [6], etc.
In order to detect design flaws early, high-level design
(engineering) models (such as UML Statecharts, BPEL [7],
AADL, SysML, etc.) are automatically mapped into dif-
ferent analysis models (such as transition systems, Petri
nets, process algebras, etc.) in order to carry out formal
verification and validation (V&V) by back-end analysis
tools. Since formal analysis models are derived by automated
model transformations, and the target analysis tools are also
typically fully automated, systems and services engineers
obtain a push-button technique for formally analyzing their
high-level design models. In the current paper, we primarily
focus on V&V tools like simulators and model checkers,
which aim at retrieving a trace as a counter-example that
violates a certain requirement.
However, such counter-example traces can be very com-
plex resulting with well over 100 elementary steps in indus-
trial scenarios. As a result, systems designers need bridge a
significant conceptual gap when they try to interpret what a
counter-example means in the original design model. Back-
annotation aims at automatically mapping back the results of
V&V tools to the original design model in order to highlight
the real source of the flaw.
Due to the semantic differences between high-level design
models and lower-level formal analysis models, we argue
in this paper that the general back-annotation problem
aiming to map a trace of a target model to a trace in
the source model can be very complicated. This is due
to the fact that most traditional source-to-target (design-
to-analysis) model transformations carry out an abstraction,
thus they are not reversible. However, in order to completely
hide the underlying formal model from systems engineers,
model-driven analysis need to provide automated support
the back-annotation of target (analysis) models to the source
(design) model.
Unfortunately, existing back-annotation approaches are
either dedicated to the source and target languages, or they
make strong assumptions on the back-annotation problem.
In the paper, we first provide a generic formulation of
the back-annotation problem (Sec. II) where back-annotation
is defined in the context of an arbitrary, but precisely
defined pair of source (design) and target (analysis) mod-
eling languages with dynamic behavior. Then we propose a
technique for the back-annotation of simulation traces based
on change-driven model transformations [8]. (1) First, simu-
lation traces of the target analysis model will be persisted as
a hierarchical change model capturing both the macro steps
and micro steps in a trace (Sec. III). (2) Then this target trace
is back-annotated to a trace of the source (design) model
using change-driven transformation rules, which bridge the
conceptual differences between macro steps in the analysis
and design traces (Sec. IV).
Our concepts will be demonstrated on the back-annotation
problem for analyzing BPEL processes using a Petri net
simulator. As a result of our back-annotation approach,
execution traces derived by a Petri net simulator can be
replayed directly on the BPEL level in order to completely
hide the underlying formal models.