Regresar

Compositional verification of business processes by model-checking

Abstract:

The work presented in this article is aimed at a contribution to the Enterprise Information Systems (EIS) verification. We describe here a Formal Compositional Verification Approach (FCVA) - based on Model-Checking (MC) techniques - applied to the verification of Business Process (BP) models represented by Business Process Modelling Notation (BPMN) diagrams. FCVA is compositional and thus allows the verification of a complex BP model carried out from verification of its parts. FCVA and a proposal of temporal semantics for BPMN allows the expression of time-dependent constructs of BP Task Models (BPTM) supported by an EIS. The interpretation of the BPMN graphical modelling entities into a formal specification language (CSP+T) allows us to use state-of-the-art MC tools to verify the behavioural part of BP models. A real-life example in the field of the Customer Relationship Management (CRM) business is presented to demonstrate the FCVA application in a practical way.