@article {SEFM10ToolDemo:back-ann,
	title = {From BPEL to SAL and Back: a Tool Demo on Back-Annotation with VIATRA2},
	year = {2010},
	note = {Accepted for the SEFM{\textquoteright}2010 "Posters and Tool Demo Session" Track
},
	month = {09/2010},
	pages = {35-42},
	institution = {Consiglio Nazionale delle Ricerche (CNR)},
	abstract = {<p>Model-driven analysis aims at detecting design\&nbsp;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\&nbsp;(V\&amp;V) tools, which may retrieve traces violating a certain\&nbsp;requirement. Back-annotation aims at mapping back the results\&nbsp;of V\&amp;V tools to the design model in order to highlight the real\&nbsp;source of the fault, to ease making necessary amendments.\&nbsp;In this tool demonstration we present an end-to-end V\&amp;V\&nbsp;tool for BPEL business processes that includes complex back-annotation support for representing V\&amp;V results as process\&nbsp;execution traces in the design environment.</p>
},
	keywords = {Viatra},
	isbn = {978-88-7958-006-9},
	url = {http://puma.isti.cnr.it/linkdoc.php?idauth=1\&idcol=1\&icode=2010-ED-003\&authority=cnr.isti\&collection=cnr.isti\&lanver=en},
	author = {{\'A}bel Heged{\"u}s and Istv{\'a}n R{\'a}th and D{\'a}niel Varr{\'o}}
}
