=Paper=
{{Paper
|id=Vol-2019/modcomp_6
|storemode=property
|title=A Multipurpose Framework for Model-based Reuse-oriented Software Integration Synthesis
|pdfUrl=https://ceur-ws.org/Vol-2019/modcomp_6.pdf
|volume=Vol-2019
|authors=Alexander Perucci,Marco Autili,Massimo Tivoli
|dblpUrl=https://dblp.org/rec/conf/models/PerucciAT17
}}
==A Multipurpose Framework for Model-based Reuse-oriented Software Integration Synthesis==
https://ceur-ws.org/Vol-2019/modcomp_6.pdf
A Multipurpose Framework for Model-based
Reuse-oriented Software Integration Synthesis
Alexander Perucci Marco Autili Massimo Tivoli
University of L’Aquila, Italy University of L’Aquila, Italy University of L’Aquila, Italy
alexander.perucci@graduate.univaq.it marco.autili@univaq.it massimo.tivoli@univaq.it
Abstract—Systems are increasingly built by reusing and inte- This paper initiates a new research and development action
grating existing software. This paper presents the preliminary that we intend to pursue towards realizing a multipurpose
version of a multipurpose framework for software integration framework for software integration synthesis. The objective
synthesis. The objective is to provide both researchers and
practitioners with an easily accessible environment that, integrat- is to provide both researchers and practitioners with an eas-
ing different kinds of software synthesizers, permit to perform ily accessible environment that, integrating different kinds
different kinds of analyses, verification, model-to-model and of software synthesizers, permit to perform different kinds
model-to-code transformations, all oriented to the reuse and the of analyses, verification, model-to-model and model-to-code
integration of existing, possibly third-party, software. transformations, all oriented to the reuse and the integration
of existing, possibly third-party, software.
I. I NTRODUCTION
With this goal in mind, we present the M ULTI S YNTH STU-
The Future Internet1 (FI) promotes a large-scale computing DIO6 , a web application7 that supports model-based synthesis
environment that will be increasingly surrounded by software of software integration code, as well as different kinds of
that, at different granularities, can be reused and composed to analysis and verification. In its preliminary version, the studio
build value added services. provides support for realizing choreography-based systems by
Systems are increasingly produced by integrating existing integrating existing software peers in a fully distributed way.
software. Furthermore, the focus of system development is The M ULTI S YNTH STUDIO offers extension mechanisms
on integration of third-parties software that exposes interfaces so to include other kind of integration synthesis methodolo-
describing the provided functionalities and the way to interact gies. That is, our mid-term goal is to include in the studio all
with them, i.e., the behavioral interaction protocol. the synthesis methodologies we have proposed in the past, so
Reuse-based software engineering is becoming the main to offer a ready-to-use integrated working environment where
development approach for building both business and com- practitioners can experiment with different synthesis method-
mercial systems [1], [2]. Numerous methodologies and soft- ologies, meeting both theoretical and practical interests.
ware engineering approaches have been proposed to address The paper is structured as follows. Section II sketches a gen-
the problem of automatic synthesis of integration code and eral picture of our multi-purpose integration synthesis method-
architectures, as well as integration paradigms and patterns [1], ology. Section III describes an instance of the general synthesis
[3]–[8]. The proposed approaches encompasses a variety of process to support the automated synthesis of choreography-
formally grounded and practical aspects, ranging from spec- based systems and its implementation. Section IV reviews
ification and analysis, from model transformation to code related work, and Section V concludes the paper.
generation, model checking and formal verification, from
implementation to run-time management. II. M ODEL - BASED S YNTHESIS OVERVIEW
During the last decade, our research activity has been
In its most general sense, a multi-purpose integration syn-
focused on model-based reuse-oriented software synthesis [2],
thesis process might involve quite different activities and
[9]–[14] for integrating (centralized or distributed) software
manipulated artifacts. Figure 1 shows a high-level activity
systems, from system architecture to composition code, from
diagrams describing the multi-purpose integration synthesis
coordination to protocol mediation/adaptation. This research
process that we have in mind.
activity has been funded by a number of national and
The System Design activity concerns the definition of
EU projects, among which the FP7 CONNECT2 , the FP7
the models to be given as input to the synthesis process.
CHOReOS and its follow-up H2020 CHOReVOLUTION3 , the
Input models can be a mix of functional models, such as
GAUSS4 and D-ASAP5 Italian PRIN projects.
(global or peer-style) interaction protocols, and non functional
1 www.future-internet.eu ones, such as security requirements and QoS constraints. For
2 www.connect-forever.eu instance, input models can be XML-based specifications of
3 www.choreos.eu – www.chorevolution.eu
4 www.lta.disco.unimib.it/GAUSS 6 The code is freely available at https://github.com/sesygroup
5 d-asap.ws.dei.polimi.it 7 multisynthstudio.disim.univaq.it
software peers by describing the interactions among them
from a global perspective. Choreographies model peer-to-peer
communication by defining a multiparty protocol that, when
put in place by the cooperating participant peers, allows for
reaching the overall choreography goal in a fully distributed
way.
Out of a choreography specification, the goal is to automati-
cally generate a set of Coordination Delegates (CDs). CDs are
additional software entities with respect to the choreography
participants, and are synthesized in order to proxify and
control the participants interaction. When interposed among
the choreography participants, CDs enforce the collaboration
prescribed by the choreography specification. The synthesized
CDs are correct by construction, meaning that the resulting
choreographed system realizes the choreography specification,
Fig. 1. Model-based Synthesis Approach even when not realizable by simply projecting the choreogra-
phy specification into each single participant [2], [9], [11]–
[13]. Our synthesis method deals with hybrid choreography
the interfaces (such as WSDL8 ) together with automata-based participants that can communicate synchronously and/or asyn-
specifications of the interaction behavior of the third-party chronously.
services/components being reused.
These models can then undergo both a Model-2-Model
Synthesis step to be transformed into intermediate models,
and/or a Model-2-Code Synthesis step to be transformed into
actual code. Examples of output (intermediate) models can
be the system architecture, coordination and adaptation mod-
els, deployment descriptor and, in general, any intermediate
representation that supports further synthesis steps or analysis
and verification. Examples of actual code can be additional
software artifacts (implemented in any programming language)
that, e.g., when integrated with the third-party software to be
composed, contribute to built the overall final system while
fulfilling the specified functional and non functional system
properties.
Both intermediate models and code can be analyzed and
verified to check, e.g., desired system properties, such as
safety and liveness, QoS requirements fulfillment, structural
properties of the input and intermediate models, and code, as
well as the system realizability. The results of the Analysis and
Verification activity can lead to reiterate the entire process, by
possibly refining input models. Fig. 2. Choreography Synthesis Approach
When the goal of the synthesis is to realize the final sys-
tem, beyond analysis and verification, the System Realization The choreography synthesis process supported by the M UL -
activity may return an overall model, e.g., specifying all the TI S YNTH STUDIO consists of the following six activities
possible interactions of the composed system, as well as, a (Figure 2), each manipulating models conforming to aptly
bundle (e.g., a Web Archive or a JAR file) containing all the defined metamodels. Model conformance ensures that each
synthesized software artifacts (e.g., coordinators, adapters and model satisfies the constraints captured in its metamodel, i.e.,
security filters) together with a description of their dependen- that the model is indeed a valid instance of the metamodel [15].
cies for actual deployment and execution.
Choreography Design – This activity concerns the definition
III. C HOREOGRAPHY S YNTHESIS of the choreography-based system to be realized. The choreog-
In this section we describe an instance of the general syn- raphy specification is given in terms of a state machine where
thesis process to support the realization of choreography-based a transition from a state to another models the exchange of a
systems. Choreographies are an emergent service engineer- message between two peers. The choreography specification
ing approach to compose together and coordinate distributed describes the way peers perform their interactions from a
global perspective by focusing on the exchange of messages.
8 https://www.w3.org/TR/wsdl Thus, a choreography specification defines the (partial) order
in which the message exchanges occur. Each message ex-
change involves two peers: the sender and the receiver of
the message. The choreography specification abstracts from
the way peers communicate to exchange messages, i.e., syn-
chronous versus asynchronous communication. The commu-
nication style will be concretized after concrete participants
(e.g., software services, software components, and things) are
selected to play the roles of the choreography peers.
Fig. 4. Choreography Specification metamodel
specification, also this model abstracts from the type of the
send and receive actions (synchronous or asynchronous). For
this reason, we call this model Abstract Participant Behavior.
Fig. 3. Sample Choreography Specification
Figure 3 shows a sample choreography specification. It
describes the interactions of the peers P1 to P6. The possible
interactions are such that P3 receives the message m1 from
P1, followed by P3 receiving the message m2 from P2. Then,
when in the branching state s2, three exclusive alternatives
can be undertaken. One alternative accounts for P6 receiving
m3 from P4, followed by P6 receiving m6 from P3, in
turn followed by P6 receiving m7 from P5. The other two
alternatives account for either P6 receiving m4 from P5, or P3
receiving m5 from P2. Each possible alternative path leads to
Fig. 5. Abstract Participant Behavior P3
the state s5, from where no more outgoing transitions can be
undertaken. The choreography specification conforms to the Figure 5 shows the abstract participant behavior of the
metamodel depicted in Figure 4. The metamodel consists of participant P3. For example, from the state s0 to s5, a possible
an arbitrary number of Messages, Participants, Transitions, and expected execution is such that P3 receives the message m1,
States. Exactly one of these states is an initial state. Each state followed by the message m2. Then, when in the branching
serves as source and/or target for a transition. Each transition state s2, one alternative is that of receiving m5.
is concretized as SendingMessageActionTransition to model
the exchange of a message between a source participant (i.e.,
the one sending the message) a target participant (i.e., the one
receiving the message).
M2M Synthesis (Projection) – Out of the choreography spec-
ification, the projection step generates one behavioral model
for each choreography peer. This model is a state machine
where a transition represents the action of either sending or
receiving a message (observable actions), or an internal action
(not observable from outside). The transition labels postfixed
with “!” represent send actions; the transition labels postfixed
with “?” represent receive actions; the label “epsilon” indicates
an internal action. For a given choreography peer, a projection
represents the behavior expected by the concrete participant
that will be selected to play the role of the choreography peer,
according to the sequences of message exchanges specified Fig. 6. Abstract Participant Behavior metamodel
by the choreography. Being derived from the choreography
Fig. 7. Abstract CD Behavior for coordinating P2 and P3
Note that we have deliberately left internal actions, which ography peers P2 and P3. The coordination logic is such that
indeed could be collapsed through an automaton simplification CD{2,3} waits for receiving a synchronization message from
procedure. The related metamodel is shown in Figure 6. CD{1,3} . Only after it can receive the message m2 from P2 and
By analyzing the metamodel, we can notice that (differently forward it to P3. When in the state “Ssynch2”, CD{2,3} send a
from the choreography metamodel in Figure 4) a message is synchronization message to CD{4,6} and CD{5,6} reaching the
concretized by OutputMessage and InputMessage in order to branch state “Sbranch2”. When in this state, three exclusive
distinguish between sent messages from received ones, respec- alternatives can be undertaken. From top to bottom, one alter-
tively. A transition is concretized by SendActionTransition, native accounts for a send synchronization message to CD{4,6}
ReceiveActionTransition, and InternalActionTransition. and CD{5,6} , followed by a send and then a receive of the
message m5; the other two alternatives account for receiving
M2M Synthesis (Coordination Logic Extraction) – This
synchronization from CD{5,6} or CD{4,6} , respectively, in turn
step takes as input the choreography specification and automat-
followed by internal actions. The coordination logic model
ically extracts the coordination logic that is required to coordi-
also conforms to the Abstract Participant Behavior metamodel
nate the choreography peers in a distributed way. The extracted
in Figure 6.
coordination logic is thus distributed into a set of Abstract
CD Behavior models. Similarly to the Abstract Participant Selection – Since our approach is reuse-oriented, the chore-
Behavior, each of them is a state machine where a transition ography is not implemented from scratch; rather, the approach
models the action of either sending a message or receiving allows to enforce the realizability of choreographies that reuse,
a message, or an internal action. As better detailed later on as much as possible, e.g., third-party services published in
this section, these actions are related to the standard com- a service inventory. Then, the selection activity consists of
munication performed to achieve the choreography business selecting concrete participants capable of playing the roles of
logic (see Figure 10). Differently from the Abstract Participant the choreography peers. This calls for exogenous coordination
Behavior, there are also transitions modeling the synchronous of the selected participants since, in general, we cannot access
exchange of coordination/synchronization messages. These their code or change it.
actions model additional communication required to realize The output of the selection phase is a set of the behavioral
the coordination logic that is needed to enforce the realizability specifications, each one defining the interaction protocol of
of the specified choreography. Standard communication takes the selected participants. A behavioral specification is also
place between a CD and the participant it controls and an automata-based model that we call Concrete Participant
supervises. When needed, additional communication messages Behavior. The related metamodel (not shown for lack of space)
are exchanged among the involved CD. is similar to the metamodel in Figure 6, with the difference
Figure 7 shows the logic of CD{2,3} coordinating the chore- that for each transition, its type is specified: synchronous,
asynchronous, or internal. m1P 1→P 3 m2P 2→P 3 m3P 4→P 6 m6P 3→P 6 m7P 5→P 6
Figure 8 shows the behavior of concrete participants se- m1P 1→P 3 m2P 2→P 3 m4P 5→P 6 m7P 5→P 6
lected for the choreography peers P 1 to P 6. The messages It is easy to see that these three traces are all allowed by the
m3, m4, m6, m7 are exchanged synchronously (graphically choreography in Figure 3. Conversely, all the traces (not com-
represented as continuous arrows); m1, m2, m5 are exchanged pletely shown in Figure 9) traversing either the state marked
asynchronously (graphically represented as dashed arrows). with (2) or the state marked with (3) are not allowed by the
choreography. Thus, according to the notion of choreography
realizability given in [16], [17], the choreography in Figure 3
is not realizable. Intuitively, this basically means that if we let
the selected participants interact in an uncontrolled way in the
composed system, they can perform interactions that are not
permitted by the choreography specification.
M2M Synthesis (Concretization) – Since the Abstract CD
Behavior is a priori generated out of the choreography speci-
fication only, it abstracts from the way the selected participants
communicate. This information is added by the Concretization
step, just after the Selection step. Interested readers can play
with the M ULTI S YNTH STUDIO web application to visualize
the resulting concrete CDs.
M2M Synthesis (System Integration) – For the set of synthe-
sized CDs, correctness by construction means that when they
are composed with the selected participants (System Integra-
tion step), the behavior of the integrated choreographed system
realizes the specified choreography. That is, the synthesized
concrete CDs enforce by construction the realizability of the
specified choreography. According to a predefined architec-
tural style, CDs are interposed among the participants needing
coordination. Figure 10 shows the instance of the architectural
style related to the sample choreography in Figure 3.
CDs perform coordination (i.e., additional communication
Fig. 8. Behavior of the Concrete Participants P1 to P6
in the figure) of the participants interaction (i.e., standard
Figure 9 shows an excerpt of the hybrid system (manually communication in the figure) in a way that the resulting
drawn) obtained by composing the set of concrete participants collaboration realizes the specified choreography. According
P 1 to P 6 in Figure 8 (the automatically generated model is to the type of actions performed by the concrete participants,
not reported here since too large in size). In Figure 8, we standard communication can be synchronous or asynchronous.
have named the states so to facilitate the mapping of the Additional communication is always synchronous. In this
choreography states in Figure 3 to the states of the hybrid sense, the system behavior is modeled as a Hybrid System
system behavior resulting from the composition in Figure 9. Behavior model. Interested readers can visualize the latter
For each participant P i, its states are labeled as P i:state-name. by using our web application. The related metamodel can be
In the hybrid system in Figure 9, asynchronous interactions found under the github repository.
(◦) are handled through messages queues all having maximum Analysis & Verification, M2C Synthesis – It is out of
size equals to 1, i.e., the participants P 1, P 2 and P 3 are all scope for this paper to discuss all the kinds of analysis and
assigned 1-bounded queues; whereas, the participant P 4, P 5 verification steps that can be performed on the generated
and P 6 are all assigned 0-bounded queues – they exchange models (beyond the fact that here we have described only
only synchronous messages (•). The participant P 3 is indeed the choreography-oriented synthesis process). Just to mention
a hybrid participant since it exchanges m6 synchronously, and a few, concrete participants behavior that model third-party
m1, m2 and m5 asynchronously. In the figure, message queues services and CDs can be analyzed and verified to check if
are denoted as [...]. Initially, all the queues are empty, hence the choreographed system can be effectively realized taking
[]. State changes and queue updates are highlighted in bold into account specified system properties. Reachability paths,
step by step. deadlock freeness, dead loops, sink states, etc, can also be
Following the branch on the left-hand side of Figure 9, three analyzed. The discussion of the different M2C transformations
different paths can be undertaken from the state marked with that can be employed is also outside the scope of this paper.
(1). The corresponding traces are: Interested reader can however refer to our previous work in [2],
m1P 1→P 3 m2P 2→P 3 m5P 2→P 3 [9]–[14].
(P1:s 0:[], P2:s 0:[], P3:s 0:[], P4:s 0:[], P5:s 0:[], P6:s 0:[])
m2P2->P3
m1P1->P3
m3P4->P6
(P1:s1:[], P2:s 0:[], P3:s0:[m1], P4:s 0:[], P5:s 0:[], P6:s 0:[])
(P1:s 0:[], P2:s2:[], P3:s0:[m2], P4:s 0:[], P5:s 0:[], P6:s 0:[])
𝜖 m3P4->P6
(P1:s 0:[], P2:s 0:[], P3:s 0:[], P4:s3:[], P5:s 0:[], P6:s3:[])
(P1:s 1:[], P2:s 0:[], P3:s1:[], P4:s 0:[], P5:s 0:[], P6:s0:[]) m1P1->P3 (P1:s 0:[], P2:s 2:[], P3:s 0:[m2], P4:s3:[], P5:s 0:[], P6:s3:[])
m2P2->P3
(3)
(P1:s1:[], P2:s 0:[], P3:s0:[m1], P4:s 3:[], P5:s 0:[], P6:s 3:[])
(P1:s 1:[], P2:s2:[], P3:s1:[m2], P4:s 0:[], P5:s 0:[], P6:s 0:[])
𝜖
𝜖
(P1:s1:[], P2:s 0:[], P3:s1:[], P4:s 3:[], P5:s 0:[], P6:s 3:[]) (2)
(1) (P1:s 1:[], P2:s 2:[], P3:s2:[], P4:s 0:[], P5:s 0:[], P6:s0:[])
m5P2->P3
m3P4->P6
(P1:s 1:[], P2:s5:[], P3:s2:[m5], P4:s 0:[], P5:s 0:[], P6:s 0:[])
m4P5->P6
𝜖 (P1:s 1:[], P2:s 2:[], P3:s 2:[], P4:s3:[], P5:s 0:[], P6:s3:[])
(P1:s 1:[], P2:s 5:[], P3:s5:[], P4:s 0:[], P5:s 0:[], P6:s0:[]) m6P3->P6
(P1:s 1:[], P2:s 2:[], P3:s5:[], P4:s 3:[], P5:s 0:[], P6:s4:[]) (P1:s 1:[], P2:s 2:[], P3:s 2:[], P4:s 0:[], P5:s4:[], P6:s4:[])
m7P5->P6 m7P5->P6
(P1:s 1:[], P2:s 2:[], P3:s 5:[], P4:s 3:[], P5:s5:[], P6:s5:[]) (P1:s 1:[], P2:s 2:[], P3:s 2:[], P4:s 0:[], P5:s5:[], P6:s5:[])
Fig. 9. An excerpt of the hybrid system composing the participants P 1 to P 6 (1-bounded queues)
Standard communication
(synchronous and/or asynchronous
P1 CD{1,3} P3 P5 message exchange)
Additional communication
P2 CD{2,3} CD{5,6} (synchronous coordination
message exchange)
Pi
CD{4,6} CD{3,6}
Concrete Participant
CD{i,j}
P4 P6
Coordination Delegate
Fig. 10. Architectural style (a sample instance of)
IV. R ELATED W ORK itors are generated through an iterative process, automatically
refining their behavior. They are first obtained by generating
The work described in this paper is related to approaches
the set of peers via choreography projection. Then, the system
and tools for automated choreography realization.
synchronizability and realizability is automatically checked
In [3], the authors propose an approach to enforce syn-
by using equivalence checking. If one of these properties is
chronizability and realizability of a choreography. The method
violated, the method exploits the generated counterexample to
implementing the approach is able to automatically generate
augment the monitors with a new synchronization message.
monitors, which act as local controllers interacting with their
Our synthesis method automatically generates CDs out of the
peers and the rest of the system in order to make the peers
choreography specification by considering that the selected
respect the choreography specification. Our notion of CD is
concrete participants are (language) equivalent to the chore-
“similar” to the notion of monitor used in [3], since CDs are
ography abstract participants. The notion of realizability that
able to interact with the choreography participants by also
we use in this paper is the same as the one used in [3] in that
performing additional communication (i.e., the exchange of
both works leverage results on choreography realizability and
Sync messages) to exogenously coordinate the participants
its decidability that are given in [16], [17].
interaction so to fulfill the choreography specification. How-
ever, the two synthesis methods are different. In [3], the mon- In [4], the authors address the realizability problem based
on a priori verification techniques, using refinement and ACKNOWLEDGMENT
proof-based formal methods. They consider asynchronous This research work has been supported by (i) the European
systems where peers communicate via possibly unbounded Union’s H2020 Programme under grant agreement number
FIFO buffers. The obtained asynchronous system is correct 644178 (project CHOReVOLUTION - Automated Synthesis
by construction, i.e., it realizes the choreography specification. of Dynamic and Secured Choreographies for the Future Inter-
With respect to our method and other methods discussed in net), (ii) the Ministry of Economy and Finance, Cipe resolution
this section, this method is more scalable in terms of number n. 135/2012 (project INCIPICT - INnovating CIty Planning
of involved peers and exchanged messages. However, our through Information and Communication Technologies), and
approach focuses on realizing a choreography specification (iii) the GAUSS national research project, which has been
by reusing third-party peers (possibly black-box), rather than funded by the MIUR under the PRIN 2015 program (Contract
generating the correct peers from scratch. This is why we 2015KWREMX).
cannot avoid to deal with exogenous coordination by means
of additional software entities such as the CDs. R EFERENCES
The approach in [5] checks the conformance between the [1] M. Güdemann, P. Poizat, G. Salaün, and L. Ye, “Verchor: A framework
choreography specification and the composition of participant for the design and verification of choreographies,” IEEE Transaction on
Services Computing, vol. 9, no. 4, pp. 647–660, 2016.
implementations. The described framework can model and [2] M. Autili, P. Inverardi, and M. Tivoli, “Automated synthesis of service
analyze compositions in which the interactions can be asyn- choreographies,” IEEE Software, vol. 32, no. 1, pp. 50–57, 2015.
chronous and the messages can be stored in unbounded queues [3] M. Güdemann, G. Salaün, and M. Ouederni, “Counterexample guided
synthesis of monitors for realizability enforcement,” in Automated Tech-
and reordered if needed. Following this line of research, nology for Verification and Analysis, ser. LNCS, S. Chakraborty and
the authors provided a hierarchy of realizability notions that M. Mukund, Eds., 2012, pp. 238–253.
forms the basis for a more flexible analysis regarding classic [4] Z. Farah, Y. Ait-Ameur, M. Ouederni, and K. Tari, “A correct-by-
construction model for asynchronously communicating systems,” Int.
realizability checks [5]. In [6], the authors identify a class of Journal on Software Tools for Technology Transfer, 2016.
systems where choreography conformance can be efficiently [5] R. Kazhamiakin and M. Pistore, “Choreography conformance analysis:
checked even in the presence of asynchronous communication. Asynchronous communications and information alignment,” in Web
Services and Formal Methods, ser. LNCS, 2006, vol. 4184.
This is done by checking choreography synchronizability. [6] S. Basu and T. Bultan, “Choreography conformance via synchronizabil-
VerChor is a framework for choreography design and verifi- ity,” in 20th WWW, 2011.
[7] M. Trainotti, M. Pistore, G. Calabrese, G. Zacco, G. Lucchese, F. Bar-
cation [1]. The framework checks a set of key properties that bon, P. Bertoli, and P. Traverso, “ASTRO: supporting composition
choreographies must respect for ensuring correctness of the and execution of web services,” in 3rd Int. Conf. on Service-Oriented
system under development, by using verification techniques Computing ICSOC, 2005.
[8] M. Carbone and F. Montesi, “Deadlock-freedom-by-design: multiparty
and tools for choreography analysis. The authors focuses asynchronous global programming,” in 40th ACM SIGPLAN-SIGACT
on asynchronous communication semantics, that is, peers POPL, 2013, pp. 263–274.
involved in the distributed system exchange messages via [9] R. Calinescu, M. Autili, J. Cámara, A. D. Marco, S. Gerasimou,
P. Inverardi, A. Perucci, N. Jansen, J. Katoen, M. Z. Kwiatkowska, O. J.
FIFO buffers. Although, in its current stage, M ULTI S YNTH Mengshoel, R. Spalazzese, and M. Tivoli, “Synthesis and verification of
STUDIO provides support to realize service choreographies self-aware computing systems,” in Self-Aware Computing Systems, 2017,
only, differently to VerChor, it has been conceived and engi- pp. 337–373.
[10] M. Autili, P. Inverardi, F. Mignosi, R. Spalazzese, and M. Tivoli,
neered to support the analysis and synthesis of reuse-based “Automated synthesis of application-layer connectors from automata-
software, which is not limited to service choreographies. based specifications,” in 9th Int. Conf. on Language and Automata
The ASTRO toolset supports automated composition of Theory and Applications LATA, 2015, pp. 3–24.
[11] M. Autili, A. D. Salle, A. Perucci, and M. Tivoli, “On the automated
Web services and the monitoring of their execution [7]. synthesis of enterprise integration patterns to adapt choreography-based
ASTRO deals with centralized orchestration-based processes distributed systems,” in 14th Int. Workshop on Foundations of Coordi-
rather than fully decentralized choreography-based ones. nation Languages and Self-Adaptive Systems FOCLASA, 2015.
[12] M. Autili, A. D. Salle, and M. Tivoli, “Synthesis of resilient chore-
In [8], the authors present a unified programming framework ographies,” in 5th Int. Workshop on Software Engineering for Resilient
for developing choreographies that are correct by construction Systems SERENE, 2013, pp. 94–108.
[13] M. Autili, D. D. Ruscio, A. D. Salle, P. Inverardi, and M. Tivoli,
in the sense that, e.g., they ensure deadlock freedom and “A model-based synthesis process for choreography realizability en-
communication safety. forcement,” in 16th Int. Conf. on Fundamental Approaches to Software
Engineering FASE, 2013, pp. 37–52.
[14] M. Autili, L. Mostarda, A. Navarra, and M. Tivoli, “Synthesis of de-
V. C ONCLUSIONS AND F UTURE W ORK centralized and concurrent adaptors for correctly assembling distributed
component-based systems,” Journal of Systems and Software, vol. 81,
no. 12, pp. 2210–2236, 2008.
This paper presented the preliminary version of the M ULTI - [15] R. F. Paige, P. J. Brooke, and J. S. Ostroff, “Metamodel-based model
S YNTH STUDIO, a multipurpose framework for software in- conformance and multiview consistency checking,” ACM Trans. Softw.
Eng. Methodol., vol. 16, no. 3, p. 11, 2007.
tegration synthesis. The studio offers extension mechanisms so [16] S. Basu, T. Bultan, and M. Ouederni, “Deciding choreography realiz-
to include other kind of integration synthesis methodologies. ability,” in 39th ACM SIGPLAN-SIGACT POPL, 2012, pp. 191–202.
Our mid-term goal is to provide both researchers and practi- [17] S. Basu and T. Bultan, “Automated choreography repair,” in 19th Int.
Conf. on Fundamental Approaches to Software Engineering FASE, 2016,
tioners with an easily accessible web-based environment that pp. 13–30.
integrates different kinds of integrator synthesis approaches.