A formalization proposal of timed BPMN for Compositional Verification of Business Processes

Abstract

The Business Process Modelling Notation (BPMN) is currently being used by companies as the Business Process (BP) standard modeling language. In this work, we define a timed semantics of BPMN in terms of the Communicating Sequential Processes + Time (CSP+T) process calculus in order to detail the behaviour of processes within a fixed time span. By adding a formal specification to the response times of activities, temporal constraints, and temporal constraints in communications and task collaboration, we are able to specify and develop the Business Process Task Model (BPTM) of a target BP. We also demonstrate how our proposal can be integrated into the Formal Compositional Verification Approach (FVCA) to allow the use of state-of-the-art MC tools to automatically verify BPTMs. Finally, we examine the application of the proposal to a BPTM verification related to the Customer Relationship Management (CRM) enterprise-business. © 2011 Springer-Verlag Berlin Heidelberg.