Conceptual framework for business processes compositional verification

doi:10.1016/j.infsof.2011.08.004

Conceptual framework for business processes compositional verification

2012-02-01

27

PRE

AI

DOI：10.1016/j.infsof.2011.08.004

原文链接

原文求助

摘要

En 中文

Context: To guarantee the success of Business Process Modelling (BPM) it is necessary to check whether the activities and tasks described by Business Processes (BPs) are sound and well coordinated. Objective: This article describes and validates a Formal Compositional Verification Approach (FCVA) that uses a Model-Checking (MC) technique to specify and verify BPs. Method: This is performed using the Communicating Sequential Processes + Time (CSP+T) process calculus, which adds new constructions to timed Business Process Model and Notation (BPMN) modelling entities for non- functional requirement specification. Results: Using our proposal we are able to specify the BP Task Model (BPTM) associated with BPs by formalising the timed BPMN notational elements. The proposal also allows us to apply MC to BPTM verification. A real-life example of verifying a BPTM in the field of Customer Relationship Management (CRM) is discussed as a practical application of FCVA. Conclusion: This approach facilitates the verification of complex BPs from independently verified local processes, and establishes a feasible way to use process calculi to verify BPs using state-of-the-art MC tools. (C) 2011 Elsevier B.V. All rights reserved.

Keyword:

Business Process Modelling

Model-Checking

Task model

Compositional verification

Formal specification

Conceptual framework for business processes compositional verification

摘要

期刊

机构

引用论文