Information Technology Reference
In-Depth Information
development style, where workflow design is accompanied by the continuous
evaluation of constraints that express domain-specific knowledge in terms of
static properties of the workflow model. In particular, the constraints can cap-
ture semantic properties of the workflow models, such as their purposes, or
rules of best practice. Similar to a spell checker in a text processing program,
which hints at the violation of orthographic rules, perhaps already indicating
a proposal for correction, the model checker notifies the workflow designer
when the defined constraints are violated.
Fig. 2.7
Extended card creation workflow
For illustration of model checking with GEAR, consider the workflow
model depicted in Figure 2.7, which extends the birthday card creation work-
flow example from Section 1.1.2: Instead of directly creating a birthday card
from a picture by applying the
draw
and
polaroid
ImageMagick services,
here the user can choose whether he wants to create a birthday card, a picture
postcard or an invitation card. For the former two cases he can furthermore
select whether to add a simple border or one in
polaroid
-style, before the
resulting image is finally saved and sent.
In terms of GEAR's logic, it can now be verified, for instance, that:
•
it is possible to create a card without using the
polaroid
effect:
EG
(
¬
“polaroid”
)
•
after loading a photo from the camera, finally the (processed) image is
saved:
“load picture from camera”
⇒
AF
(
“save”
)
•
if the user has selected to create a birthday card, the suitable text is added:
[
“birthday card”
](
AF
(
“add happy birthday”
))
Search WWH ::
Custom Search