Regresar

Choreography modeling compliance for timed business models

Abstract:

Business Process Modeling (BPM) is a conceptual activity for embodying the functioning and complex structure of any enterprise’s business processes, so that these can be then analyzed and improved. A BP can be understood as a set of related, structured, interacting services driven by a choreography that is capable of giving complex functionality to customers. General choreographies of BP cannot be verified, specially timed choreographies, because implementations scarcely show the same behavior than the one initially specified according to business rules. We therefore propose here a formal semantics for a subset of BPMN, in order to check if a given choreography is realizable. This includes formalization of behavioral and temporal aspects of BPMN. A set of transformation rules for choreography diagrams into a timed process algebra is given. Therefore, we obtain an easy verification approach for choreography implementation models based on model–checking tools. In this way we can obtain advantage of the strengths that a formalization of behavioral and temporal aspects of BPMN will bring about, at design and implementation stages, to any model of interest.