Verifying Compliance of Business Processes with Temporal Answer Sets
Verifying Compliance of Business Processes with Temporal Answer Sets
复制标题
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
D. D'Aprile;Laura Giordano;Valentina Gliozzi;A. Martelli;G. Pozzato;D. T. Dupré
中科院分区：
文献类型：
--
作者：
D. D'Aprile;Laura Giordano;Valentina Gliozzi;A. Martelli;G. Pozzato;D. T. Dupré
在本文中，我们提供了一个业务流程规范和验证的框架，该框架基于答案集编程（ASP）的时间扩展，并解决了验证业务流程是否符合规范的问题。我们使用的逻辑形式主义是答案集编程和动态线性时态逻辑 (DLTL) 的组合，并允许通过一组时态规则和一组时态约束对业务流程进行声明性规范以及规范规范。承诺的概念借用了代理沟通的社会方法，用于捕获规范内的义务。除了允许业务流程的声明性规范之外，所提出的框架还可用于对以传统工作流语言指定的业务流程进行编码。对由时间公式表示的业务流程的时间属性的验证可以通过在 ASP 中编码有界模型检查技术来完成。验证业务流程是否符合规范尤其包括验证业务流程的执行是否不存在留下承诺的情况
In this paper we provide a framework for the specification and the verification of business processes, which is based on a temporal extension of answer set programming (ASP) and we address the problem of verifying the compliance of business processes to norms. The logical formalism we use, is a combination of Answer Set Programming and Dynamic Linear Time Temporal Logic (DLTL), and allows for a declarative specification of a business process, as well as the specification of norms, by means of a set of temporal rules and a set of temporal constraints. A notion of commitment, borrowed from the social approach to agent communication, is used to capture obligations within norms. Besides allowing for a declarative specification of business processes, the proposed framework can be used for encoding business processes specified in conventional workflow languages. The verification of temporal properties of a business process, expressed by temporal formulas, can be done by encoding bounded model checking techniques in ASP. Verifying compliance of a business process to norms consists, in particular, in verifying that there are no executions of the business process which leave commitments