Automating the transformation from BPMN models to CSP plus T specifications

The complexity of modern Business Process Modelling (BPM) together with the absence of the appropriate validation tools is the main reason for the costly and non-evolutionary characteristics of these models. Temporal constructs of Extended Business Process Model and Notation (EBPMN) semantics are disambiguated here by using Communicating Sequential Processes+Time (CSP+T) process calculus, which adds new constructions to timed BPMN modelling entities for non-functional requirements specification. Our objective is to facilitate the description of a business process model as a collection of verified software components, thereby advancing to their complete verification with state-of-the-art model checking tools. One real-life example, Customer Relationship Management (CRM) modelled as a correct business task model is discussed to demonstrate the applicability of the verification approach.