Regresar

Business process automatic verification with a compositional approach

Abstract:

Currently, complex Business Processes (BP) are implemented by Enterprise Information Systems (EIS). However, the development of EIS is complicated if there is no guarantee the reliability of the Task Model (TM) of the PN. This article describes the Formal Compositional Verification Approach (FCVA), an infrastructure for the formal specification and verification of BP, supported by Model Checking (MC) techniques. Based on a proposal for a temporal formal semantics for the Business Process Model and Notation (BPMN), which allows us to obtain the MT of a business process, the EFVC supports MT behavior verification from the individual verification of their participants. The interpretation of notational elements of BPMN in the Communicating Sequential Processes + Time (CSP+T) formal language allows us to incorporate MC tools widely used to verify the behaviour of a TM. A real-life example in the field of the Customer Relationship Management (CRM) business is presented to demonstrate the FCVA application in a practical way.