Abstract: |
In any organisation, properties such as scope, structure, deployment, capability, structural consistency and concurrency, supporting the critical factors for success in Business Process (BP) modelling, need to be verified. And thus, relevant parts of a BP must be formally specified in an appropriate way. Process Calculi (PC) such as CSP, ACP, CCS, which constitute a mathematical basis for programming reactive, communication-bounded systems, can be used to model critical systems and to verify their correctness properties. PC-based notations can be used to specify business processes (BPs) and reason about their properties. Without a demanding training, to make use effectively of these languages is beyond the ability of many business modellers. In order to cope with this drawback, we propose a set of rules to automatically transform a semi-formal model expressed in terms of Business Process Modelling Notation (BPMN) into a Communicating Sequential Processes + Time (CSP+T) formal system specification. In this paper, we present BTRANSFORMER tool that permits to automatically generate such a formal specification and has been programmed with the ATLAS Transformation Language (ATL). As result, we obtain a plug-in for Eclipse platform, which is capable of transforming BPMN models designed with Intalio into a text file with the equivalent CSP+T formal specification of the business model. |