TY - GEN
T1 - Compositional modeling and verification of workflow processes
AU - Voorhoeve, M.
PY - 2000
Y1 - 2000
N2 - Workflow processes are represented as Petri nets with special entry and exit places and labeled transitions. The transition labels represent actions. We give a semantics for such nets in terms of transition systems. This allows us to describe and verify properties like termination: the guaranteed option to terminate successfully. We describe the composition of complex WF nets from simpler ones by means of certain operators. The simple operators preserve termination, giving correctness by design. Only the advanced communication operators are potentially dangerous. A strategy for verification of other properties is described.
AB - Workflow processes are represented as Petri nets with special entry and exit places and labeled transitions. The transition labels represent actions. We give a semantics for such nets in terms of transition systems. This allows us to describe and verify properties like termination: the guaranteed option to terminate successfully. We describe the composition of complex WF nets from simpler ones by means of certain operators. The simple operators preserve termination, giving correctness by design. Only the advanced communication operators are potentially dangerous. A strategy for verification of other properties is described.
U2 - 10.1007/3-540-45594-9_12
DO - 10.1007/3-540-45594-9_12
M3 - Conference contribution
SN - 3-540-67454-3
T3 - Lecture Notes in Computer Science
SP - 184
EP - 200
BT - Business Process Management: Models, Techniques, and Empirical Studies
A2 - Aalst, van der, W.M.P.
A2 - Desel, J.
A2 - Oberweis, A.
PB - Springer
CY - Berlin
ER -