Modeling Interaction-Oriented Architectures using Choreographies

Abstract

The Software architecture of a system can be regarded as a consistent set of views to describe the system. This paper focuses on the interaction between components in a system. These can be modeled as choreographies, capturing all allowed interactions between the components. In this paper, we show that it is feasible to analyze a composed set of these choreographies: a tree of choreographies in which each member may refer to another. The two major components of the analysis are correctness by structure: a choreography needs to follow strict rules to guarantee soundness. Otherwise, the choreography is transformed into a Petri net which is checked by an external tool. This paper shows the theoretical techniques to verify a composed choreography, and implements the solutions into a single educational modeler tool: INORA2.

Keywords

• eol>Petri nets
• Software architecture
• Model-checking
• Choreographies
• BPMN

1. Introduction

to model the flow of information. Although there is a clear relation between the features in the FAM and the activities in the BPMN diagrams, creating and maintaining this mapping is a manual task, and thus remains error prone.

Architectural Description Languages (ADLs) combine diferent views and notations to assist the architect in creating a consistent description of a system. However, their main disadvantage is that they typically require to model the complete system to be able to reason over the system. As such, their overhead in modeling very quickly becomes rather a burden than an advantage [ 4 ]. Another disadvantage is that most ADLs are only semi-formal, i.e., they do not allow for formal analysis of properties, such as the absence of deadlocks and livelocks.

In this paper, we build upon the ideas described in [ 5 ], and introduce the interaction-oriented software architecture (INORA). It combines a functional view on the system to describe the organisation of the software elements, with choreographies [ 6 ] to model the interactions between these elements. These choreographies are automatically translated into a set of components that allow for formal verification using LoLA [ 7 ]. Rather than modeling the complete system in a formal notation, the architect only needs to design the component interactions. As a choreography only describes a single conversation between a set of participants, the proposed approach allows to realise the choreographies into a single system automatically. As we show, if the architect limits themselves in the used constructs, the approach guarantees correctness by design.

The remainder of this paper is structured as follows. In the next section, we introduce Open Nets, a class of Petri nets to model asynchronously communicating systems upon which our approach builds. Section 3 discusses choreographies and their translation to Petri nets. In Section 4, we present INORA and discuss its framework and tool support. Last, Section 5 concludes the paper, discussing limitations of the approach and future work.

2. Asynchronously Communicating Systems

In this section, we introduce the basic notions of Petri nets, and show how these can be used to model Open Nets, that are used to reason over the communication between components.

2.1. Basic Notions

Let and be possibly infinite sets. The powerset of is denoted by () = {′ | ′ ⊆ } and || denotes the cardinality of . Sets and are disjoint if ∩ = ∅, with ∅ denoting the empty set. Given disjoint sets and , and sets and , the composition of two functions : → and : → , denoted by ∪ , is defined by ( ∪ )() = () if ∈ and ( ∪ )() = () if ∈ .

A sequence over of length ∈ N is a function : {1, . . . , } → where where N = {0, 1, 2, 3, . . .} describes the set of all natural numbers, including 0. If > 0 and () = , for 1 ≤ ≤ , we write = ⟨1, . . . , ⟩. The length of a sequence is denoted by | |. The sequence of length 0 is called the empty sequence, and is denoted by . The set of all finite sequences over is denoted by * . We write ∈ if there is 1 ≤ ≤ | | such that () = .

A Petri net is a tuple = (, , ) with and two disjoint sets of places and transitions, respectively, and a flow relation ⊆ ( × ) ∪ ( × ). The elements of ∪ are called the nodes of . Elements of are called arcs. Places are depicted as circles, transitions as squares. For each element (1, 2) ∈ an arc is drawn from 1 to 2. Given a node ∈ ∪ , we define its preset ∙ = { | (, ) ∈ } and its postset by ∙ = { | (, ) ∈ }. If the context is clear, we omit the subscript.

A marking of is a function : → N that describes the configuration of tokens in each of the places of . The set of all possible markings of is denoted by M( ). A Petri net with corresponding marking is written as (, ) and is called a marked Petri net. Given a marked Petri net (, ), a transition is enabled if all its input places contain at least one token, i.e., ∀ ∈ ∙ : () > 0. An enabled transition can fire . Firing transition results in a new marking ′, denoted as (, )[⟩(, ′), with ′() + ((, )) = () + ((, )) with ( ) = 1 if ∈ and ( ) = 0 otherwise. We lift Firing of transitions to sequences in a standard way. A sequence ∈ * is called a firing sequence from (, 0) if markings 1, . . . exist such that (, − 1)[ ()⟩(, ) for all 1 ≤ ≤ | |. The set of all reachable markings from (, ) is defined by ℛ(, ) = {′ | ∃ ∈ * : (, )[ ⟩(, ′)}.

Several classes of Petri nets exist. A Petri net (, , ) is called a state machine if |∙ | ≤ 1 and ∙ | ≤ 1 for all places ∈ . It is called a marked graph if |∙ | = |∙ | = 1 for all transitions ∈ . A workflow net is a tuple = (, , , , ) with (, , ) a Petri net, ∈ its initial place such that ∙ = ∅, ∈ its final place such that ∙ = ∅ and all nodes ∈ ∪ are on a path from to . A workflow nets is called sound if (1) [ ] ∈ ℛ(, []) and (2) ( ) > 1 =⇒ = [ ] for all ∈ ℛ(, []), where [] denotes the marking with a single token in place , i.e., []() = 1 if = and []() = 0 otherwise.

2.2. Open Nets and Their Composition

A set of asynchronously communicating components interact via message passing: messages are sent and received by components. The approach we follow is based on Open Nets [ 8 ]. In an Open Net, message passing is modeled via interface places. An interface place is either an input place, receiving messages from other components, or an output place, that sends messages to other components.

Definition 1 (Open Net). An Open Net is a tuple (, , , , , , Ω) where • ( ∪ ∪ , , ) is a Petri net; • is the set of internal places; • is the set of input places, such that ∙ = ∅; • is the set of output places, such that ∙ = ∅; • Transitions are connected to at most one interface place: |(∙ ∪ ∙ ) ∩ ( ∪ )| ≤ 1 for all ∈ ; • Any interface place is connected to at most one transition: |∙ ∪ ∙ | = 1 for all ∈ ∪ ; • : → N is the initial marking; and • Ω ⊆ → N is the set of final markings . Places ∪ are called the interface of . The skeleton of considers without its interface places, and is defined by ( ) = (, , ). If ( ) is a state machine, is called an S-Net.

As transitions are connected to at most one interface place, each transition has a sign, indicating whether the transition sends or receives messages from the interfaces. Definition 2 (Sign). Let = (, , , , , , Ω) be an Open Net. The sign of a transition is defined by the function sign : → { !, ?, } such that for any transition , sign() = ! if ∙ ∩ ̸= ∅, sign() = ? if ∙ ∩ ̸= ∅ and sign() = otherwise. If the context is clear, the subscript is omitted.

As correctness notion for Open Nets, we extend soundness to the internal behavior of an Open Net, i.e., the skeleton of the Open Net should be weakly terminating and properly completing. Definition 3 (Soundness). Let = (, , , , , , Ω) be an Open Net. It is sound if: • ( ) is weakly terminating, i.e., ∀ ∈ ℛ(( ), ) an ∈ Ω exists such that ∈ ℛ(( ), ); and • ( ) is properly completing, i.e., ∀ ∈ ℛ(( ), ) if an ∈ Ω exists such that () ≤ () for all places ∈ , then = .

Figure 1 shows two Open Nets, and . Both nets share five interface places, , , , , and . Places , and are output places for and input places for . Similarly, places and are input places for and output places for . Net has four additional interface places: input places ℎ and , and output places and . If the set of final marking is the singleton set containing the initial marking, then both and are sound.

Two Open Nets can be composed if their interfaces match: an input place of the one should be an output place of the other, and vice versa. Their composition glues the common interface places, which become internal places in the composition.

Definition 4 (Composition). Given two Open Nets = ( , , , , , , Ω ) and = ( , , , , , , Ω ) are composable, denoted by ⊕ , if and only if ( ∪ ∪ ∪ ) ∩ ( ∪ ∪ ∪ ) = ( ∩ ) ∪ ( ∩ ).

Their composition is again an Open Net, denoted by ⊕ = (, , , , , , Ω) with • = ∪ ∪ ; • = ( ∪ ) ∖ ; • = ( ∪ ) ∖ ; • = ∪ ; • = ∪ ; • () = ∪ ; • Ω = { ∪ | ∈ Ω , ∈ Ω }; where = ( ∩ ) ∪ ( ∩ ).

Consider nets and in Fig. 1. Their intersection only contains interface places of and such that input places of are an output place of , and vice versa. Hence, nets and are composable, resulting in ⊕ , where places , , , and are internal places.

3. Modeling Interactions

As shown in the previous section, Open Nets can be used to model asynchronously communicating systems. Two types of approaches can be identified for designing such systems. The first type is to first create and verify the complete model and then divide it into separate components (cf. [ 9 ]). The second type is to model the components individually, verify the individual components, and then compose them (cf. [ 10 ]). The problem of the former is that it is very dificult to maintain such models: once created and updated, the complete model needs to be revisited and changes need to be tracked to the components. The problem of the latter is that compositional verification is very hard [ 11, 12 ] and in general even undecidable [ 13 ]. One solution is to limit the expressive power of models, thus guaranteeing soundness by construction [ 14 ]. All these approaches have in common that the resulting model describe the inner working of components, instead of their interactions. A diferent perspective on modeling the interaction between components, is to design the message flow using choreographies. To analyse choreographies, two properties need to be analysed: first, the message flow itself should be sound, and second,

BPMN Start event

ParticipantP message A

Participant Q Participant A sends message MAB1 to Participant B there should exist a set of components that together can realise the message flow [ 15 ]. In the remainder of this section, we introduce choreographies, and show one approach to generate a possible realisation that can be verified. In addition, we show that for a specific class that are realisable by construction: the structure of the choreography ensures its realisability.

3.1. Choreographies

Instead of modeling the behavior of individual components, choreographies models the flow of messages between components [ 6 ]. An activity in a choreography resembles an interaction between a sender and receiver via a message. In this way, the execution of a choreography resembles a message-based conversation between a set of participants. A choreography describes the set of all possible conversations between these participants. In our setting, these participants resemble software elements.

As of BPMN 2.0, a specific notation is added to support modeling choreographies. Similar to BPMN, gateways are used to direct the message flows. Although many diferent types of gateways exist, we follow the 7 process modeling guidelines [ 16 ], and limit the gateways to only exclusive choice (XOR) and parallelism (AND). An example choreography is shown in Fig. 2. In this example, two participants, and , communicate. First Participant sends message to Participant , after which Participant either sends message , or message . After this choice, both participants send a message to the other: participant sends message and participant sends message . Note that although BPMN adds an envelope icon to depict the messages explicitly, we leave them out for readability.

3.2. Transformation to Petri Nets

As choreographies do not have a formal semantics, diferent translations exist to transform choreographies to formal notations, such as Pi calculus [ 17 ], Event B [ 18 ], and Petri nets [ 19, 20 ]. An important property for choreographies is realisability: whether a set of components exist that together implement exactly the same set of conversations as specified by the choreography [ 15 ]. In general, this property is undecidable [ 21, 15 ]. Instead, we follow a practical approach, and generate for each participant a Petri net based on the choreography, and verify soundness on their composition. Although this does not guarantee realisability, it provides a necessary correctness check. In this paper, we rely on the translation to Petri nets. Following the ideas of [ 14 ], our proposed transformation consists of four steps: 1. Translate the choreography into a Petri net; 2. Duplicate the Petri net for each participant; 3. Generate for each message a place; 4. Connect the message places to each participant, based on their sign.

Table 1 shows the transformation rules to generate a Petri net from a choreography. The translation is inspired by the existing translations [ 19, 20 ]. However, the transformation rule for the XOR gateways difers in our setting. Instead of using silent transitions for each input and output arc, we translate the XOR gateway to1a32single place. Although this translation would generate erroneous models in general [ 20 ], it is required for interaction-based models. As an example, consider the choreography depicted in Fig. 3a. If in this choreography the XOR gateway would be translated into two silent transitions, one for each leg, the resulting model would become unsound, as both participants may choose a diferent leg. Instead, each choice needs to be controlled by one of the participants [ 14 ].

In the second step, the generated Petri net is duplicated for each participant. Each transition is annotated with the message it sends or receives. For the example choreography shown in Fig. 3a, this results in two participant nets. Next, for each message, a place is generated. These are the colored places in Fig. 3b. Next, for each transition in the participant the corresponding message is connected: if in the choreography participant sends a message , then the corresponding transition in the participant net produces a token in place . Similarly, if in the choreography participant receives a message , then the corresponding transition in the participant net consumes a token from place . This results in a a composable set of Open Net, one for each participant, as shown in Fig. 3b.

3.3. Correctness by Construction

In general, the proposed translation does not guarantee soundness: If the choreography is sound, it is not necessarily the case that the resulting composition is sound. For example, if two participants can choose diferent legs of an XOR gateway, the choreography itself is sound, but the composition is not. In this section, we show that for a class of choreographies, the proposed transformation guarantees soundness.

State machines have only choices, and no concurrency. As shown in [ 22 ], any state machine workflow net is sound and safe. For Open Nets, a similar property holds: any S-Net is sound and safe. However, that does not guarantee that the composition of two S-Nets is sound. The proposed translation results in identical Open Nets for each participant, i.e., for each two participants, their Open Nets are isomorphic. As shown in [ 14 ], the composition of two isomorphic S-Nets yield a sound model under certain conditions: for any interface places a corresponding pair of isomorphic transitions should exist, in any choice, the sign of all transitions should be the same, and any loops should contain both sending and receiving transitions. If these conditions are met, we say that the composition agrees on the isomorphism. Definition 5 (Composition agrees on isomorphism [ 14 ]). Given two S-Nets = (, , , , , , Ω ) and = (, , , , , , Ω ) such that their skeletons are isomorphic with respect to relation , their composition = ⊕ agrees on if and only if: 1. for all transitions ∈ , ′ ∈ , a place ∈ exists such that {(, ), (, ′)} ⊆ or {(′, ), (, )} ⊆ if and only if () = ′; 2. all transitions in the postset of a place have the same sign, i.e., for all places ∈ , we have: sign(1) = sign(1) for all transitions 1, 2 ∈ ∙ ; 3. for all markings ∈ ℛ((), ) and non-empty firing sequences ∈ * such that ((), )[ ⟩((), ), transitions , ∈ exist such that sign() = ! and sign() = !. Theorem 1 (Soundness of Isomorphic S-Nets [ 14 ]). Let and be two S-Nets such that their skeletons are isomorphic with respect to relation , and their composition ⊕ agrees on . Then ⊕ is sound.

In the remainder of this section, we translate these results of Open Nets to choreographies. We say a choreography is well-behaving if: 1. it has two participants; 2. it contains exactly one start event and one end event; 3. all activities are on a path from the start event to the end event; 4. all activities have exactly one input and one output arc; 5. all its gateways are XOR, i.e., the choreography does not contain any parallellism; 6. all activities directly after an XOR gateway have the same sending participant; 7. in any loop each participant sends at least one message; . In other words, the translation of a well-behaving choreography results in an S-Net. Theorem 2. A well-behaving choreography is sound.

Proof. Let and be the two participants of the choreography. By rules 2-5, the transformation rules of Table 1 return a state machine net . By step 2 of the algorithm, two participant nets and are constructed. As these nets are both isomorphic with , and hence, and are isomorphic as well. By steps 3 and 4 of the algorithm, any message place is between two isomorphic transitions, thus satisfying the first condition of Definition 5. Rules 6 and 7 of well-behaving choreographies correspond to the second and third condition of Definition 5. Hence, the composition ⊕ agrees on the isomorphism, and thus ⊕ is sound.

4. Interaction-oriented Architectures

Choreographies describe all allowed conversations between a set of participants. In a software system, not all software elements participate in all conversations, and many conversations are repeated frequently, for example to send regular notifications. Architects typically model these smaller “subconversations” rather than creating a large model that contains all possible interactions. Creating such a model is very tedious and error-prone. In addition, verification becomes very expensive as the many interleavings of independent conversations result in a state explosion. Therefore, we propose Interaction Oriented Architecture (INORA), a a systematic approach to design and analyze complex interactions between software elements. INORA allows for modeling both the static and dynamic aspects in one model. It consists of an Interaction Model and a set of Protocols.

The meta model of INORA is presented in Fig. 4. It consists of three parts: the Interaction Model, the BPMN Choreography Diagrams, and the Representation, i.e., the views created by the architect.

lnteraction Oriented

Architecture .

.

parent _, O.*represents.- 1..1 ◄ ► -.iOn.s*tance of -1..1 .

4.1. Interaction Model

The Interaction Models allows for defining the organization of components and displaying the allowed interactions between those components. It provides an overview of the organization and the interactions in the system to create a clear picture of the system as a whole. An Interaction Model consists of zero or many containers. A container is either composite, i.e., it contains one or more other containers, or it is atomic, i.e., it contains one or more functions (C2). We define the parent, where parent( a , b ) entails that is the parent of . The container cannot contain itself or any of its parents (C1). The Interaction Model references zero or more protocols. A protocol has at least two roles.

Protocols can be re-used between diferent functions. Therefore, we introduce the concept protocol instance, which refers to a protocol. functions can participate in a protocol instance in a role as defined by the corresponding protocol. Only one participant can instantiate a protocol instance (C3). This results in the following constraints on the meta model:

C1 The transitive closure of is irreflective;

C2 A Container can either contain other Containers or one or multiple Functions; Component 1

Component 1 F1 A F2

F4 C F3

F1 A F2

F4 C F3 B

B i : {B} i : {C} Component 2

Component 3

Component 2

Component 3

C3 At most one Participant can instantiate a Protocol Instance.

An Interaction Model contains zero or more Protocols. A protocol is defined as a Choreography consisting of a set of Activities and zero or more events. Each Activity contains two roles: a sender and a receiver. An event refers to the execution of another protocol, and thus allows for a hierarchy of protocols that are being executed to fulfill a protocol. Protocols can be expressed in any modeling language that allows for the following concepts:

1. A message with a sender and a receiver.

2. A notion of choices in the execution path of the protocol. 3. A modeling element that can represent a using-relation or another protocol.

INORA supports having multiple views or representations of a single Interaction Model definition. Formally, an Interaction Model can be represented by zero or more Views. Each view contains zero or more Nodes. This allows us to hide certain nodes from a view. It is, for example, possible to hide entire containers in a view to only show a certain part of the system.

4.2. Notation and Semantics

Figure 5 shows a view of an Interaction Model. The view depicts three containers: Component 1, Component 2 and Component 3. Component 1 consists of 2 functions, 1 and 4. Function 1 participates with function 2 of Component 2 in protocol , function 2 participates in protocol with function 3 of Component 3. Function 4 also participates with function 3, in protocol . In INORA, we assume all protocol compositions to be trees. In other words, if a function participates in two protocols, the function is duplicated for each protocol, as shown in the right hand side of Fig. 5.

Events are used to model a hierarchical composition of choreographies, as shown in Fig. 6. As we only allow trees of choreographies, functions do not depend on each other, thus ensuring no cyclic dependencies can occur. In this way, INORA allows for compositional verification of the system. As each refined protocol only communicates with other functions, a tree is constructed following the principles as defined in [ 14 ]. Consequently, if each of the protocols is sound, the complete interaction model is sound.

Can Check-in Cannot Check-in

PTC System - Auth

M: OK Trip Terminal - Auth PTC System - Auth M: Insuff. Balance Trip Terminal - Auth Protocol D End

Protocol D Start

Trip Terminal - Auth M : RMeeqsuseasgteCMhe1ck-in PTC System - Auth

Handle Auth Trip Terminal - Auth requests check-in from PTC System - Auth

Unauthorised PTC System - Auth Authorized M : Authorised Trip Terminal - Auth

Protocol B PTC System - Auth M M:ResesgaisgterMT1rip PTC System - Trip

Get Trip

OK Insuff.

Balance

PTC System - Auth M : Error message

Trip Terminal - Auth PTC System - Trip M: Can check-in PTC System - Auth PTC System - Trip M: Cannot check-in

PTC System - Auth Protocol B Start Protocol B End

4.3. Tool Support

To support the translation and verification methods, a tool has been developed: INORA2 2. The tool ofers the following main functionalities: 1. modeling the interaction model (Fig. 7); 2. modeling and maintaining protocols as choreographies (Fig. 8); 3. automatically generating Petri nets and choreography trees; 4. running an step-wise analysis chain to verify whether protocol compositions are “correct” (Fig. 9).

A user generally creates or loads a project, after which the interaction model must be populated. The interaction model is the core of the project, as it creates the functionalities and their components, and defines the hierarchy between them. Protocols are the detailed views for each arc in the interaction models. Both these models can be modeled out in INORA2. The tool also ofers quality-of-life features to help users quickly draw out the interaction flows in 2The tool is freely available from: https://git.science.uu.nl/interaction-oriented-architecture

BPMN choreography format. When both the interaction model is (partially) populated, and the necessary protocols are modeled out the user can kick-of an analysis.

The tool first tries to do a static analysis on the choreography, before it uses LoLA [ 7 ] to analyse the translated Petri net. The analysis window starts a chain of events. First, it creates the composition. Using the protocol on which the analysis is run as a starting position, it constructs the reference tree by recursively finding all protocols that can be reached by reference. All of the referred protocols need to be sound for the composition to be sound. Therefore, let be a composition referring to protocol B, all protocols in the composition = {, }, () = {( → )} are checked for soundness.

Secondly, the syntax of the protocol is checked. The tool checks for example whether each protocol has a single start and end event, and whether all activities have a single input and output arc. If all constraints hold, the semantics of the protocol is checked. Then, INORA2 tries to generate a choreography tree. This proves correctness by construction. The protocol does need to conform to very strict additional constraints, so the generation of the tree may fail if there is a violation of the constraints.

The last step is to translate the choreography to a Petri net and verify their correctness using DAME LoLA. It sends the Petri net to DAME LoLA and runs a list of formulae. For the first version of INORA2, the decision was made to only check for weak termination. Let be all the places in a Petri net and Ω ⊂ all places that are end-event outputs, the formula used is: ( (∀ ∈ Ω : () = 1 ∧ ∀ ∈ ∖ Ω : () = 0)) Finally, a conclusion is drawn on the soundness of the protocol. In case the protocol is not sound, the architect can analyse the underlying Petri net, as shown in Fig. 9.

5. Conclusions

In this paper, we propose Interaction-Oriented Architectures to model a system of asynchronously communicating systems. In an Interaction-Oriented Architecture, the communication between software elements is modeled using choreographies. The interaction model consists of a set of choreographies, such that if each of the choreographies is sound, the overall interaction model is sound. To analyse the choreographies, we rely on Open Nets. We show that if choreographies are well-behaving, a sound realisation exists, i.e., based on the structure of the choreography, a sound realisation can be derived. The approach is implemented in the tool INORA2, which supports the architect to design interaction models and choreographies. Under the hood, the tool uses both syntax checkers as well as LoLA to verify correctness. The tool demonstrates that it is feasible to use these techniques in modelers. Currently, the implemented checks are limited to checking for weak termination: checking if all tokens from the initial marking eventually always end up in all the end places, without any lingering tokens. There is a wide variety of possible model-checking formulas, such as proper completion. In the future, we want to extend the tool to allow the architect to define and verify their own, additional formulae.

As the tool shows, it is feasible to automatically model-check interaction models and their protocols. Though the steps, translations, and evaluations seem correct, we have not conducted a case study or consulted professionals for their opinions. The developed tools (INORA2 and DAME LoLA) are currently released as educational tools. Although they are developed with usability in mind, it is not professionally developed software.

A limitation of the study is the visual representation of the generated feedback. We have achieved a way to automatically translate, verify and display it outcomes in the INORA tool, yet it lacks a way to display the information on the diagram itself. Although LoLA provides an evidence path, and our mapping can translate this to a firing sequence in the translated model, no visualisations exist that display the Petri net firing sequence on top of a choreography. Providing more advanced feedback by translating the results of formal analysis techniques to the architect is an essential next step.

References

[1] L. Bass , P. Clements , R. Kazman , Software architecture in practice , Addison-Wesley Professional , 2003 .

[2] N. Rozanski , E. Woods, Software systems architecture: working with stakeholders using viewpoints and perspectives , Addison-Wesley, 2012 .

[3] S. Brinkkemper , S. Pachidi , Functional architecture modeling for the software product industry , in: M. A. Babar , I. Gorton (Eds.), ECSA 2010 , volume 6285 of Lecture Notes in Computer Science, Springer, 2010 , pp. 198 - 213 . URL: https://doi.org/10.1007/978-3- 642 -15114-9_ 16 . doi: 10 .1007/978-3- 642 -15114-9\_ 16 .

[4] I. Malavolta , P. Lago , H. Muccini , P. Pelliccione , A. Tang , What industry needs from architectural languages: A survey , IEEE Trans. Software Eng . 39 ( 2013 ) 869 - 891 . URL: https://doi.org/10.1109/TSE. 2012 . 74 . doi: 10 .1109/TSE. 2012 . 74 .

[5] J. M. E. M. van der Werf , E. Kaats, Discovery of functional architectures from event logs , in: D. Moldt , H. Rölke , H. Störrle (Eds.), International Workshop on Petri Nets and Software Engineering (PNSE'15) , volume 1372 of CEUR Workshop Proceedings, CEUR-WS.org , 2015 , pp. 227 - 243 . URL: https://ceur-ws. org/ Vol- 1372 /paper13.pdf.

[6] G. Decker , M. Weske , Interaction-centric modeling of process choreographies , Inf. Syst . 36 ( 2011 ) 292 - 312 . URL: https://doi.org/10.1016/j.is. 2010 . 06 .005. doi: 10 .1016/j.is. 2010 . 06 .005.

[7] K. Wolf , Petri net model checking with lola 2 , in: International Conference on Applications and Theory of Petri Nets and Concurrency , Springer, 2018 , pp. 351 - 362 .

[8] P. Massuthe , A. Serebrenik , N. Sidorova , K. Wolf , Can i find a partner? undecidability of partner existence for open nets , Information Processing Letters 108 ( 2008 ) 374 - 378 .

[9] W. M. P. van der Aalst , N. Lohmann, P. Massuthe , C. Stahl , K. Wolf , Multiparty contracts: Agreeing and implementing interorganizational processes , Comput. J . 53 ( 2010 ) 90 - 106 . URL: https://doi.org/10.1093/comjnl/bxn064. doi: 10 .1093/comjnl/bxn064.

[10] M. D. McIlroy , J. Buxton , P. Naur , B. Randell , Mass-produced software components , in: Proceedings of the 1st international conference on software engineering , Garmisch Pattenkirchen, Germany, 1968 , pp. 88 - 98 .

[11] J. M. E. M. van der Werf , Compositional verification of asynchronously communicating systems , in: I. Lanese , E. Madelaine (Eds.), Formal Aspects of Component Software - 11th International Symposium, FACS 2014 , Bertinoro, Italy, September 10-12 , 2014 , Revised Selected Papers, volume 8997 of Lecture Notes in Computer Science, Springer, 2014 , pp. 49 - 67 . URL: https://doi.org/10.1007/978-3- 319 -15317- 9 _4. doi: 10 .1007/978-3- 319 -15317-9\_4.

[12] K. Wolf , C. Stahl , D. Weinberg , J. Ott , R. Danitz , Guaranteeing weak termination in service discovery , Fundam. Informaticae 108 ( 2011 ) 151 - 180 . URL: https://doi.org/10.3233/ FI-2011-417. doi: 10 .3233/FI-2011-417.

[13] K. Wolf , Does my service have partners?, Transactions on Petri Nets and Other Models of Concurrency II: Special Issue on Concurrency in Process-Aware Information Systems ( 2009 ) 152 - 171 .

[14] K. M. van Hee , N. Sidorova , J. M. E. M. van der Werf , Construction of asynchronous communicating systems: Weak termination guaranteed! , in: B. Baudry , E. Wohlstadter (Eds.), Software Composition - 9th International Conference, SC@TOOLS 2010 , Malaga, Spain, July 1-2 , 2010 . Proceedings, volume 6144 of Lecture Notes in Computer Science, Springer, 2010 , pp. 106 - 121 . URL: https://doi.org/10.1007/978-3- 642 -14046- 4 _8. doi: 10 . 1007/978-3- 642 -14046-4\_8.

[15] N. Lohmann , K. Wolf , Decidability results for choreography realization , in: G. Kappel, Z. Maamar , H. R. M. Nezhad (Eds.), Service-Oriented Computing - 9th International Conference, ICSOC 2011 , Paphos, Cyprus, December 5- 8 , 2011 Proceedings , volume 7084 of Lecture Notes in Computer Science, Springer, 2011 , pp. 92 - 107 . URL: https://doi.org/10. 1007/978-3- 642 -25535- 9 _7. doi: 10 .1007/978-3- 642 -25535-9\_7.

[16] J. Mendling , H. A. Reijers , W. M. van der Aalst, Seven process modeling guidelines (7pmg) , Information and software technology 52 ( 2010 ) 127 - 136 .

[17] F. Abouzaid , J. Mullins , Formal specification of correlation in WS orchestrations using bp-calculus , in: Proceedings of the 5th International Workshop on Formal Aspects of Component Software, FACS 2008 , Malaga, Spain, September 10-12 , 2008 , volume 260 of Electronic Notes in Theoretical Computer Science, Elsevier, 2008 , pp. 3 - 24 . URL: https: //doi.org/10.1016/j.entcs. 2009 . 12 .029. doi: 10 .1016/j.entcs. 2009 . 12 .029.

[18] H. A. Le , N. Truong , Modeling and verifying WS-CDL using event-b, in: Context-Aware Systems and Applications - First International Conference, ICCASA 2012, Ho Chi Minh City , Vietnam, November 26-27 , 2012 , Revised Selected Papers, volume 109 of Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering , Springer, 2012 , pp. 290 - 299 . URL: https://doi.org/10.1007/978-3- 642 -36642-0_ 29 . doi: 10 . 1007/978-3- 642 -36642-0\_ 29 .

[19] R. M. Dijkman , M. Dumas , C. Ouyang , Semantics and analysis of business process models in BPMN, Inf . Softw. Technol. 50 ( 2008 ) 1281 - 1294 . URL: https://doi.org/10.1016/j.infsof. 2008 . 02 .006. doi: 10 .1016/j.infsof. 2008 . 02 .006.

[20] I. Raedts , M. Petkovic , Y. S. Usenko , J. M. E. van der Werf , J. F. Groote , L. J. Somers , Transformation of bpmn models for behaviour analysis ., MSVVEIS 2007 ( 2007 ) 126 - 137 .

[21] K. Wolf , Decidability issues for decentralized controllability of open nets , in: M. Schwarick , M. Heiner (Eds.), Proceedings of the 17th German Workshop on Algorithms and Tools for Petri Nets , Cottbus, Germany, October 07-08 , 2010 , volume 643 of CEUR Workshop Proceedings, CEUR-WS.org , 2010 , pp. 124 - 129 . URL: https://ceur-ws. org/ Vol- 643 /paper14. pdf.

[22] K. M. van Hee , N. Sidorova , M. Voorhoeve , Soundness and separability of workflow nets in the stepwise refinement approach , in: Applications and Theory of Petri Nets 2003 , 24th International Conference, ICATPN 2003, Eindhoven, The Netherlands , June 23-27, 2003 , Proceedings, volume 2679 of Lecture Notes in Computer Science, Springer, 2003 , pp. 337 - 356 . URL: https://doi.org/10.1007/3-540-44919-1_ 22 . doi: 10 .1007/3-540-44919-1\_ 22 .