Model Checking Analysis of Semantically Annotated Business Processes

Model Checking Analysis of Semantically Annotated Business Processes
复制标题

DOI：
10.1109/tsmca.2012.2183357
复制
发表时间：
2012-07
期刊：
IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans
影响因子：
--
通讯作者：
María José Ibáñez;Javier Fabra;P. Álvarez;J. Ezpeleta
María José Ibáñez;Javier Fabra;P. Álvarez;J. Ezpeleta
中科院分区：
其他
文献类型：
--
作者：
María José Ibáñez;Javier Fabra;P. Álvarez;J. Ezpeleta

文献摘要

被引文献

相似文献

语义业务流程需要新的分析技术，能够处理也考虑语义方面的行为属性。本文介绍了一种模型检测方法，该方法在模型描述和待验证公式中都包含了语义方面。此外，形式化地定义了一元资源描述框架(RDF)注释的Petri网系统，它是一种允许使用RDF注释对业务流程进行语义描述的形式，并用于表示模型检查器的输入模型。最后，给出了基于RDF和SPARQL工具的一元RDF注解的PETRI网形式化描述和模型检测框架的原型实现。
Semantic business processes require new analysis techniques able to deal with behavioral properties that also consider semantic aspects. In this paper, a model checking method is introduced including semantic aspects in both the model description and the formula to be verified. In addition, Unary resource description framework (RDF) annotated Petri net systems, a formalism that allows the semantic description of business processes using RDF annotations, is formally defined and used to represent the input model of the model checker. Finally, the prototype implementations of both the Unary RDF annotated Petri net formalism and a model checker framework based on the use of RDF and SPARQL tools are also presented.