From BPEL to SAL and Back: a Tool Demo on Back-Annotation with VIATRA2

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. In this tool demonstration we present an end-to-end V&V tool for BPEL business processes that includes complex back-annotation support for representing V&V results as process execution traces in the design environment.