Conceptual framework for business processes compositional verification

[Display omitted] ► Business Process Modelling (BPM) supported by compositional formal languages. ► Modelling, specification, and verification of Business Process Task Model (BPTM). ► BPTM design process based on compositional strengths of CSP process algebra. ► Integration of Model-Checking (MC) te...

Full description

Saved in:
Bibliographic Details
Published in:Information and software technology 2012-02, Vol.54 (2), p.149-161
Main Authors: Mendoza, Luis E., Capel, Manuel I., Pérez, María A.
Format: Article
Language:English
Subjects:
Business
Business Process Modelling
Business process reengineering
Calculi
Calculus
Compositional verification
Customer relationship management
Formal specification
Mathematical models
Model-Checking
Modelling
Program verification (computers)
Proposals
Studies
Task model
Tasks
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:[Display omitted] ► Business Process Modelling (BPM) supported by compositional formal languages. ► Modelling, specification, and verification of Business Process Task Model (BPTM). ► BPTM design process based on compositional strengths of CSP process algebra. ► Integration of Model-Checking (MC) technique with the BPTM design process. 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. This article describes and validates a Formal Compositional Verification Approach (FCVA) that uses a Model-Checking (MC) technique to specify and verify BPs. 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. 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. 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.
ISSN:0950-5849
1873-6025
DOI:10.1016/j.infsof.2011.08.004