Information Technology Reference
In-Depth Information
Specification Formula
The specification formula describes all sequences of services that meet the
individual workflow specification, but without taking care of actual executabil-
ity concerns. It is given declaratively as a formula in SLTL, a semantically en-
riched version of the commonly known propositional linear-time logic (PLTL)
that is focused on finite paths. The syntax of SLTL is defined by the following
BNF, where
t
c
and
s
c
express type and service constraints, respectively:
φUφ
Thus, SLTL combines static, dynamic, and temporal constraints. The
static constraints are the taxonomic expressions (boolean connectives) over
the types or classes of the type taxonomy. Analogously, the dynamic con-
straints are the taxonomic expressions over the services or classes of the ser-
vice taxonomy. The temporal constraints are covered by the modal structure
of the logic, suitable to express the ordering constraints:
• s
c
φ
states that
φ
must hold in the successor state, and that it must be
reachable with service constraint
s
c
.
φ
::=
true
|
t
c
|¬
φ
|
φ
∧
φ
|
s
c
φ
|
Gφ
|
•
G
expresses that
φ
must hold generally.
U
specifies that
φ
1
has to be valid until
φ
2
finally holds.
In addition to the operators defined above, it is convenient to derive further
ones from these basic constructs, such as the common boolean operators
(disjunction, implication, etc.), the eventually operator F
φ
=
def
true
U
φ
,or
the weak until operator
φ
WU
ψ
=
def
(
φ
U
ψ
)
•
G(
φ
). Furthermore, the next
operator X
φ
is often used as an abbreviation of
∨
φ
.Acompleteformal
definition of the semantics of SLTL can be found, for instance, in [301, 178].
The distinctive feature of SLTL formulae is that they cover two dimensions:
1. The
horizontal
dimension, covered by the modalities that describe as-
pects of relative time, addresses the workflow model, including its loosely
specified parts, and deals with the actual service sequences.
2. The
vertical
dimension evaluates taxonomic expressions over types and
services, allowing for the usage of abstract type and service descriptions
within the specifications.
Both kinds of constraints can deliberately be combined in order to express
more complex intents about the workflows. This allows for a very flexible
fine-tuning of the workflow specifications.
The specification formula that is finally used as input for the synthesis algo-
rithm is simply a conjunction of all available SLTL constraints, comprising:
•
true
The definition of the
start condition(s)
of the workflow (i.e., the set of
data types that is available at the beginning).
•
The definition of the
end condition(s)
of the workflow (i.e., the set of data
types that must be available at the end of the synthesized workflow).
•
The set of available
workflow constraints
.
Search WWH ::
Custom Search