Business process verification using a Formal Compositional Approach and Timed Automata

Several firms are defining their Business Processes (BPs) using the standard Business Process Model and Notation (BPMN). BPs modelled with BPMN are maintained and used by different workers within a company, thus the correctness of critical BPs should be validated and verified. In this work we present how Model Checking verification technique for software has been integrated within a Formal Compositional Verification Approach (FVCA) and Timed Automata (TA) to allow the automatic verification of critical BPs modelled with BPMN. The use of our FVCA support business analysts and designers in the formal specification of BP-task model with TA. The application of the FVCA is aimed at guaranteeing the correctness of the BP-task model with respect to initial properties specification derived from business rules. In order to show a practical use of our proposal and Uppaal tool, one instance of an enterprise-project related to Customer Relationship Management business is discussed.