语义标识的过程模型的可执行性分析

Formal Analysis the Executability of Semantically Annotated Process Model

语义标识的过程模型是基于领域本体对过程模型中活动的前置条件&效果进行标识后所产生的模型.语义过程模型的可执行性问题是确保语义过程模型质量的核心问题,同时已被证明是一个co-NP难问题.基于关联变量集模型定义了语义过程模型的动态语义;定义了该动态语义的命题公式的编码规则;提出了基于可满足性求解器的可执行性分析方法;该方法能判定可执行性问题同时当模型不满足可执行性时能反馈出有问题的活动;此外,实现了相应的原型工具SPMT,该工具支持对语义过程模型的建模及可执行性分析;最后通过实际例子对以上理论及工具进行了有效性验证.

Semantically annotated process model （SPM） is a process model with semantic annotations, i. e. , precondition＆effect, la- beled for its activities based on the domain ontology. However, SPM analysis is challenging, since its correctness is beyond the soundness of process model and its state transition needs to care about domain state change. To assuring the correctness of SPM, the executablity analysis is essential and has also been identified as a coNP-hard problem. To tame the hardness of the executability, a dy- namic semantics for SPM, based on related variables set model, is proposed for defining domain state transition; an encoding method is presented by which the semantics is encoded into formulae as well as the executability. Meanwhile, a procedure, based on SAT solver, is proposed through which the executability can be bounded model checked and diagnosed. Our method has been implemented as a tool called SPMT. The experiment results show our method is valid and SAT solver is very efficient.