Affiliations: Institute of Informatics, University of Warsaw, Poland.
sroka@mimuw.edu.pl | Faculty EEMCS, Delft University of Technology, The
Netherlands. a.j.h.hidders@tudelft.nl
Note: [] Address for correspondence: Institute of Informatics, University
of Warsaw, Banacha 2, 02-097 Warsaw, Poland
Abstract: Workflow development and enactment workbenches are becoming a
standard tool for conducting in silico experiments. Their main advantages are
easy to operate user interfaces, specialized and expressive graphical workflow
specification languages and integration with a huge number of bioinformatic
services. A popular example of such a workbench is Taverna, which has many
additional useful features like service discovery, storing intermediate results
and tracking data provenance. We discuss a detailed formal semantics for Scufl - the workflow
definition language of the Taverna workbench. It has several interesting
features that are notmet in other models including dynamic and transparent type
coercion and implicit iteration, control edges, failure mechanisms, and
incominglinks strategies. We study these features and investigate their
usefulness separately as well as in combination, and discuss alternatives. The formal definition of such a detailed semantics not only allows
to exactly understand what is being done in a given experiment, but is also the
first step toward automatic correctness verification and allows the creation of
auxiliary tools that would detect potential errors and suggest possible
solutions to workflow creators, the same way as Integrated Development
Environments aid modern programmers. A formal semantics is also essential for
work on enactment optimization and in designing the means to effectively query
workflow repositories. This paper is the second of two. In the first one [13] we have
defined, explained and discussed fundamental notions for describing Scufl
graphs and their semantics. Here, in the second part, we use these notions to
define the semantics and show that our definition can be used to prove
properties of Scufl graphs.
