Integration Verification of Workflow Business Rule Semantic

Workflow model must be described correctly to guarantee successful execution at runtime. So verification technology of model is important and can be classified into syntactic, structural, and semantic. The strictest and highest-level verification is the semantic one which has not been solved well yet in the workflow research. Futhermore, correctness of control logic depends on business semantic, and is one of the influence factors on structual soundness. By analyzing business rules and their constraint parts described in workflow model, business rules semantic can be formalized to expression. So verifying semantic integrality of business rules can be converted into that of constraint sets. Constraint sets are used to decide which path is chosen to execute. If a constraint set described in a condition node in workflow model misses some semantics and expresses redundant or meaningless semantics, these can also cause erroneous structure, which is one of the important factors executing unsuccessfully. Domain of universe coverability theorem and decision-tree-based verification arithmetic are put forward to verify the semantic integrality of constraint sets, and then the structrual soundness of workflow model is ensured by this method. This verification technology is independent of specific modeling mothods, so that complete commonality, modeling-independentce, and wide applicability are the three advantages of this verification method.