工作流业务规则语义的完整性验证技术

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 describ.ed 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.