Formalization and Animation of Business Process Collaborations.

The increasing adoption of modeling methods contributes to the better un- derstanding of the flow of processes from the internal behavior of a single organization to a wider perspective where several organizations exchange messages. In this regard, the BPMN standard provides a suitable abstrac- tion for modeling, analyzing, executing, and monitoring business processes within the same organization or involving multiple ones. Even if this is a widely accepted notation, a major drawback of BPMN is related to the complexity of the semi-formal definition of its meta-model. Moreover, only limited efforts have been expended in formalizing its exe- cution semantics, especially for what concerns the interplay among control features, data handling and exchange of messages in scenarios requiring mul- tiple instances of interacting participants. Consequently, the modeling of a BPMN diagram, as well as fully understanding of its behavior, may result very difficult in presence of such concepts. Thus, providing a formal semantics of the BPMN notation is crucial for shaping collaborative systems and guaranteeing that these systems behave as they are supposed to. Moreover, figuring out the interplay between control flow, messages, and data, by looking at static process models, is in general error-prone and time-consuming. In this regard, visualization techniques, such as animation, can effectively support the designer. In addition, a formal semantics gives the possibility to simulate business processes. This thesis faces these problems by providing a formal semantics for BPMN collaborations that includes elements dealing with multiple instances, i.e., multi-instance pools and sequential/parallel multi-instance tasks. Be- yond defining a novel formalization, the thesis proposes solutions that exploit this formalization to dynamically visualize the behavior and the business con- text of BPMN diagrams through 2D and 3D animation, and for generating event logs from the simulation of business processes.