Workflows Require Verification
Useability, Safety, Liveness
in Web Service Compositions
Useability: workflow achieves objectives.
Request
Ψ
is true in the final state.
I.e., in final state
S
f
, ∃ {W
i
}, {S
i
< S
f
} | ∪{E(W
i
)} ⊨ Ψ
Safety: nothing bad ever happens.
∀ W
i
called in state
S
i
, P(W
i
)
are true in
S
i
.
And no constraints are violated.
Liveness: good things keep happening (no Deadlock).
Msg ∈ Input(W
i
) ∧ Msg ∈ Output(W
j
) ⇒ (S
i
≥ S
j
)
If, as
defined
,
Input(W) ∈ P(W)
and
Output(W) ∈ E(W)
,
then Liveness follows from Safety.
However, many approaches do not do this, and so
must check for correct message exchange separately
from verifying that all preconditions are met.
©2012
Charles Petrie
- permission to reproduce widely with attribution.
