# A Choreography-Based and Collaborative Road Mobility System for L'Aquila City
## 2 Related Work  
The approach described in this paper is mainly related to the automated choreography realization. VerChor is a framework for choreography design and verification [13]. The framework translates the existing choreography languages, i.e., conversation protocols or BPMN 2.0 choreographies, into the LOTOS NT (LNT) process algebra [24] by means of a choreography intermediate format (CIF). In this way, the framework exploits the analysis techniques provided by the CADP [25] toolbox to check a set of key properties that choreographies must respect for ensuring correctness of the system under development. Our approach leverages on theoretical results exploited in [13] to provide practical and automatic support for the realization of reuse-based service choreographies and hence to boost the adoption of choreographies in the development practices adopted by IT companies. [PERSON] et al. [26] propose a method to enforce synchronizability and realizability of a choreography. The method generates monitors that, similarly to our notion of CD, act as distributed controllers. However, the synthesis technique is different from ours in that monitors are generated by iteratively refining their behavior. [PERSON] et al. [27] identify a class of systems where choreography conformance can be efficiently checked even in the presence of asynchronous communication. This is done by checking synchronizability. The approach characterizes relevant properties to check choreography realizability that represents the starting point for choreography realizability enforcement. However, it is focused on a fundamentally different problem from ours. It statically checks realizability and does not account for its automatic enforcement at run time, including code synthesis, actual deployment and execution. The ASTRO toolset supports automated composition of services [28]. It aims to compose a service out of a business requirement and the description of available external services. More specifically, a planner component automatically synthesizes the code of a centralized process that achieves the business requirement by interacting with the available external services. Unlike our approach, ASTRO deals with orchestration-based processes rather than decentralized choreography-based ones. The CIGAR (Concurrent and Interleaving Goal and Activity Recognition) framework is for multigoal recognition [29]. It decomposes an observed sequence of multigoal activities into a set of action sequences specifying whether a goal is active in a specific action. Goal recognition concerns learning a model of an agent by observing the agent's actions while interacting with the environment. In contrast, realizability enforcement decentralizes the coordination logic specified by choreography. [PERSON] et al. [30] present a unified programming framework for developing choreographies that ensure deadlock freedom and communication safety. Developers design both protocols and implementation from a global perspective. Correct endpoint implementations are then automatically generated. [PERSON] et al. [31] discuss some of the extensions of the Jolie orchestration language. Differently from our approach, they focus on developing choreographies from scratch, rather than realizing them through service reuse. [PERSON] et al. use a game theoretic approach for checking whether incompatible component interfaces can be made compatible by inserting a converter between them which satisfies specified requirements. This approach is able to automatically synthesize the converter [32]. In contrast to our method, their method needs as input a deadlock-free specification of the requirements that should be satisfied by the adapter, by delegating to the user the non-trivial task of specifying that. Our validation phase, automatically achieve deadlock freeness in the choreography specification. [PERSON] and [PERSON] presented an approach that, exploiting ontology reasoning and constraint programming, allows for automatically inferring mappings between components interfaces [33].