From BPEL to SAL and Back: a Tool Demo on Back-Annotation with VIATRA2
|Title||From BPEL to SAL and Back: a Tool Demo on Back-Annotation with VIATRA2|
|Year of Publication||2010|
|Authors||Hegedüs, Á., Ráth, I., and Varró, D.|
|Institution||Consiglio Nazionale delle Ricerche (CNR)|
Model-driven analysis aims at detecting design ﬂaws early in high-level design models by automatically de-riving mathematical models. These analysis models are sub-sequently investigated by formal veriﬁcation 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.
Accepted for the SEFM'2010 "Posters and Tool Demo Session" Track