Analisi e sintesi automatica di coreografie di servizi usando Reti di Petri Colorate

Nowadays we are surrounded by a rapidly increasing number of software applications and systems that provide different services in various domains. They are often built by reusing and integrating existing services that are distributed all over the internet, promoting a reuse-based software production. To this end, there are two approaches for service composition: orchestration and choreography. The former is a centralized approach, while the latter is a fully distributed one. Services involved in a choreography are composed and coordinated from a global perspective by specifying their external interactions in terms of peer-to-peer message exchanges. In general, developing the distributed coordination logic that is required to let the participant services collaborate correctly is a difficult and error prone task, especially when dealing with third-party services, typically black-box. Research works in the state of the art, carried on within the EU FP7 CHOReOS and the EU H2020 CHOReVOLTUION projects, address this issue by proposing the automated synthesis of distributed Coordination Delegates (CDs). They are additional software entities that, when interposed among the participant services, control their interaction in order to fulfill the collaboration prescribed by a choreography specification, which can be either BPMN2-compliant or LTS-based. BPMN2 Choreography Diagrams represent the current standard de-facto for modeling choreographies. However, being an industrial notations, often used for documentation and design purposes only, Choreography Diagrams lack of formal semantics, leading to many different interpretations by researchers and practitioners proposed in the state of the art. On the other hand, in the literature there exist many formal notations that have been found profitable for modeling and analyzing distributed systems, although too often, differently from researches, practitioners are not much inclined to use them. Colored Petri Nets (CPNs) is one of these notations. In this Ph.D. dissertation, a rigorous mapping from BPMN2 Choreography Diagrams to Colored Choreography Nets (CCNs) is presented. CCNs represent an enhanced and revised version of CPNs conceived for enabling simulation, analysis and automated synthesis of service choreographies. Furthermore, we propose a novel synthesis method for realizing CCNs choreographies and, hence, leveraging the defined mapping, also BPMN2 choreographies. Moreover, these CCNS choreographies undergo deadlock-free analysis and differently from the synthesis in the state of the art, this synthesis method simplifies the general approach specially in dealing with synchronicity and asynchronicity due to the characteristics of CCNs. The work has been validated through the application of the approach at work on several examples borrowed from CHOReVOLUTION case studies and through scenario simulation via the CPNTools.