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

TitleFrom BPEL to SAL and Back: a Tool Demo on Back-Annotation with VIATRA2
Publication TypeReport
Year of Publication2010
AuthorsHegedüs, Á., Ráth, I., and Varró, D.
Pagination35-42
Date Published09/2010
InstitutionConsiglio Nazionale delle Ricerche (CNR)
ISBN Number978-88-7958-006-9
KeywordsViatra
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. 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.

NotesAccepted for the SEFM'2010 "Posters and Tool Demo Session" Track
URLhttp://puma.isti.cnr.it/linkdoc.php?idauth=1&idcol=1&icode=2010-ED-003&authority=cnr.isti&collection=cnr.isti&lanver=en
PDF: