Search

For designing and analyzing complex workflow nets the notion of hierarchical decomposition can be essential for keeping the structure of the workflow comprehensible. In this paper we study two classes of nets: hierarchical nets and extended hierarchical nets. The first have a simple hierarchical structure and can be defined in terms of five simple refinement rules. We show that for arbitrary nets it can be easily verified if they can be constructed this way, thus confirming their good design and the properties following from it. As we prove, this can be done by performing the refinements in reverse, i.e., by contracting subnets into single nodes. It is shown that the choice of the contracted subnet does not change the final result of the process, and therefore this procedure for checking the hierarchical structure requires no back-tracking. The second class, extended hierarchical nets, is an extension of the first class where two types of extra refinements are introduced that allow to indicate (1) the synchronization between two parallel running subworkflows or (2) the transfer of a thread from one subworkflow to another one. These refinements come with natural and necessary preconditions that ensure that result is still a sound workflow net. In case (1) where we want to synchronize two actions in two subworkflows, we should convince ourselves that the subworkflows represent parallel threads which always execute together, otherwise a deadlock could easily arise. Dually, in case (2), if after the moment that a choice was made between two subworkflows we at a later point in the workflow want to allow a transfer between them, this can be done safely provided that we did not enter any thread fork in the meantime. We show that the class of extended hierarchical nets, which is defined by adding these two additional types of refinement, is a proper superset of the hierarchical nets, but still all such nets exhibit the correctness property of *-soundness. We do this by showing that the class is a proper subset of the AND-OR nets which were in earlier work shown to have this property. [ABSTRACT FROM AUTHOR]

Abstract: We present a method for hierarchically generating sound workflow nets by substitution of nets with multiple inputs and outputs. We show that this method is correct and generalizes the class of nets generated by other hierarchical approaches. The method involves a new notion of soundness which is preserved by the generalized type of substitution that is presented in this paper. We show that this notion is better suited than ⁎-soundness for use with the presented type of generalized substitution, since ⁎-soundness is not preserved by it. It is moreover shown that it is in some sense the optimal notion of soundness for the purpose of generating sound nets by the presented type of substitution. [Copyright &y& Elsevier]

Abstract: This paper presents a formal semantics for the Taverna 2 scientific workflow system. Taverna 2 is a successor to Taverna, an open-source workflow system broadly adopted within the e-science community worldwide. The new version improves upon the existing model in two main ways: (i) by adding support for data pipelining, which in turns enables input streams of indefinite length to be processed efficiently; and (ii) by providing new extensibility points that make it possible to add new operators to the workflow model. Consistent with previous work by some of the authors, we use trace semantics to describe the effect of workflow computations, and we show how they can be used to describe the new features in the Taverna 2 model. [Copyright &y& Elsevier]

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 first of two. It defines, explains and discusses fundamental notions for describing Scufl graphs and their semantics. Then, 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. [ABSTRACT FROM AUTHOR]

Abstract: In this paper we propose DFL—a formal, graphical workflow language for dataflows, i.e., workflows where large amounts of complex data are manipulated, and the structure of the manipulated data is reflected in the structure of the workflow. It is a common extension of (1) Petri nets, which are responsible for the organization of the processing tasks, and (2) nested relational calculus, which is a database query language over complex objects, and is responsible for handling collections of data items (in particular, for iteration) and for the typing system. We demonstrate that dataflows constructed in a hierarchical manner, according to a set of refinement rules we propose, are semi-sound, i.e., initiated with a single token (which may represent a complex scientific data collection) in the input node, terminate with a single token in the output node (which represents the output data collection). In particular they never leave any “debris data” behind and an output is always eventually computed regardless of how the computation proceeds. [Copyright &y& Elsevier]