Paper Info
Title
Back-annotation of Simulation Traces with Change-Driven Model Transformations
Abstract
Model-driven analysis aims at detecting design flaws early in high-level design models by automatically deriving mathematical models. These analysis models are subsequently 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 simulation 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.
Year
DOI
Venue
2010
10.1109/SEFM.2010.28
SEFM
Keywords
Field
DocType
Petri nets,formal verification,specification languages,BPEL process,Petri net simulator,automatically deriving mathematical model,backannotation problem,change driven model transformation,design flaw detection,formal validation tool,formal verification,high level design model,model driven analysis,simulation trace,back-annotation,change-driven model transformations,simulation traces
Petri net,Programming language,Unified Modeling Language,Computer science,Theoretical computer science,Business Process Execution Language,Mathematical model,Back annotation,Macro,Semantics,Formal verification
Conference
Citations 
PageRank 
References 
21
0.79
17
Authors
4
Name
Order
Citations
PageRank
Abel Hegedus1371.80
Bergmann, G.2210.79
Istvan Rath3644.37
Dániel Varró41682118.10