The Bio-jETI Framework - User-Level Workflow Design: A Bioinformatics Perspective - page 46

2.3.1 The Synthesis Method

Generally, the term process synthesis is used to refer to techniques that
construct workflows from sets of services according to logical specifications
[196, 119]. The algorithm that is used by PROPHETS is based on the modal
logic SLTL (Semantic Linear Time Logic) that combines relative time with
descriptions and taxonomic classifications of types and services [305, 97, 98].
It takes two aspects into account: On the one hand, the workflow must en-
sure a valid execution regarding type correctness, on the other hand, the
constraints specified by the workflow designer must be met.
The algorithm had already been implemented for the predecessors of the
current jABC and jETI frameworks, that is, for the ABC and ETI platforms
[98, 207], and was recently also used in the scope of the Semantic Web Ser-
vices Challenge [248] for synthesizing mediators between different message
formats [198, 159]. Only with the introduction of PROPHETS, however, the
synthesis method has become conveniently accessible also for “normal” users:
Background knowledge about the underlying method is not required for us-
ing the plugin, since all formal specifications that the synthesis algorithm
needs are derived automatically from the intuitive, graphical specification
mechanisms that PROPHETS provides.
Hence, knowledge of the internal details of the synthesis algorithm is not
required in the scope of this topic, and accordingly this section is restricted
to sketching the basic ideas of how the algorithm works. Concretely, the
following describes how the synthesis universe (which constitutes the search
space in which the synthesis algorithm looks for solutions to the synthesis
problem) is built from the provided domain model, how SLTL is used for the
abstract workflow specification formula ,andwhatthe synthesis algorithm can
finally derive from this information. For further details the reader is referred
to [305].

Synthesis Universe

The synthesis method relies on behavioral service interface descriptions, that
is, services are regarded as transformations that perform particular actions
on the available data. Concretely, each service interface description must
characterize the service by means of four subsets of the set of all data types:

• USE are the types that must be available before execution of the service

(i.e. the input types of the service),

• FORBID describes a set of types that must not be available before exe-

cution of the service,

• GEN is the set of types that are created by the execution of the services

(i.e. the output types of the service),

• KILL defines those types that are destroyed and therefore removed from

the set of types that were available prior to execution of the service.