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

Formal Analysis the Executability of Semantically Annotated Process Model

作　　者：龚平[1] 蒋建明[1] 张仕[1] 

机构地区：[1]福建师范大学数学与计算机科学学院,福州350007

出　　处：《小型微型计算机系统》2012年第12期2618-2624,共7页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61100017)资助;福建省自然基金项目(2012J05112)资助;福建省教育厅A类项目(JA10080;JA11069)资助

摘　　要：语义标识的过程模型是基于领域本体对过程模型中活动的前置条件&效果进行标识后所产生的模型.语义过程模型的可执行性问题是确保语义过程模型质量的核心问题,同时已被证明是一个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.

关 键 词：语义标注过程模型 可执行性 有界模型检查 可满足性求解器 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]