Automatic Compositional Verification of Business Processes

Nowadays the Business Process Modelling Notation (BPMN) has become a standard to provide a notation readily understandable by all business process (BP) stakeholders when it conics to carrying out the Business Process Modelling (BPM) activity. In this paper, we present a new Formal Compositional Verification Approach (FCVA), based on the Model-Checking verification technique for software, integrated with a formal software design method called MEDISTAM-RT Both are used to facilitate the development of the Task Model (TM) associated to a BP design. MEDISTAM-RT uses UML-RT as its graphical modelling notation and CSP+T formal specification language for temporal annotations. The application of FCVA is aimed at guaranteeing the correctness of the TM with respect to initial property specification derived from the BP rules. One instance of a BPM enterprise-project related to the Customer Relationship Management (CRM) business is discussed in order to show a practical use of our proposal.