Keywords

1 Introduction

Business Process Management (BPM) systems [20, 23] are widely used to automate organizational business processes. Organizations rely on BPM to analyze, control or optimize their processes. BPM systems provide means for automated process analysis such as model validation, transformation, simulation, visualization of key performance indicators, and reporting [3]. Despite the variety of BPM systems  [21, 29], The foundation of BPMN is based on Petri Nets [1, 32]. The choice of Petri Nets as foundation for BPMN implementation over other formal methods, often more expressive or specialized [13, 14], is not surprising: hardly any model is as simple, intuitive, and naturally supports task traceability.

While Petri net-based models enable automated process analysis, they lack a few desirable characteristics: (i) They cannot naturally represent semantics of component-based or service-based processes. Ideally, we would like to plug semantic models for individual components (often integrated dynamically at run time) to the semantic models of existing processes in a compositional way. (ii) The classical Petri Nets are not expressive enough and often are extended (e.g., with colors, reset and inhibitor arcs, priority transitions) to enable meaningful process analysis. Such extensions change the semantics of the model and generate incompatible dialects of process-specification languages adopted by various tools.

An alternative formalization to express the semantics of BPMN models is the Reo coordination language [5]. Reo has been used to formalize semantics of BPMN, UML Activity and Sequence Diagrams [15], to map BPEL fragments [33], to represent transactional workflows [27], and to implement service orchestrations [24] and service choreographies [30]. Reo allows composition of components and services in an intuitive way, and addresses the issue (i) mentioned above. Moreover, the open-ended nature of Reo allows us to introduce channels with specific properties required for some applications. Introducing new primitives may make it necessary to extend the formal semantics of Reo in order to include some new concepts. Several dozen variations of semantic models for Reo have been proposed [25]. They vary from rather simple ones that cover basic Reo behavior (e.g., constraint automata  [8]) to more complex models that cover specific behavioral aspects, e.g., context-sensitivity [18]. In some of these models, computing the overall semantics of a system is computationally expensive. This hampers using the language for analyzing large real-world business processes.

In [16], the authors proposed to model the semantics of Reo as a constraint satisfaction problem (CSP). They define data flow in a Reo network in the form of mathematical expressions on data observed at Reo nodes. The main advantage of such representation is the possibility to use existing constraint solvers to infer the behavior of a network given the semantics of its constituent parts.

Priority flow is an important aspect of process modeling, which is not easily supported by existing formalisms. Analyzing compensation and error handling requires a mechanism to express priority of some flow alternatives over others. In this paper, we propose a constraint-based framework for priority flow. There is ongoing work on an existing automata based formal semantics of Reo to handle priority, but our practical needs for dealing with large models of realistic business processes currently complicates direct use of automata-based semantic models.

This paper is organized as follows: In Sect. 2, we briefly describe the Reo coordination language. In Sect. 3, we introduce priority flow in Reo along with a constraint-based semantics for it. In Sect. 4, we extend our approach to support numeric priorities. In Sect. 5, we show the application of our constraint-based approach via two classes of connectors: (a) priority-aware, and (b) connectors with a large number of states. In Sect. 6, we overview related work. Finally, in Sect. 7, we conclude the paper and outline future work.

2 Reo

In the realm of service-oriented computing, the behavior of a software system is not only defined by the functionality of its services, but also by their interactions. The code written to realize the latter is often called glue code. Writing and maintaining glue code is a tedious task, especially in complex systems wherein the size and rigidity of the glue code tend to grow over time. Coordination languages offer a more manageable alternative for generating glue code. Reo [5, 6] is a channel-based coordination language for composition of software components and services. Using a small and open-ended set of predefined and user-defined constructs, Reo supports modeling of complex coordination behavior.

The primitive constructs in Reo are channels and nodes, whose composition yields connectors. A channel is an atomic connector with two ends and a constraint that relates the flow of data at these ends. Channel ends are either source ends that read data into the channel or sink ends that write the channel’s data out. Channels can connect to each other through nodes. There are two types of channel ends; therefore, three types of nodes can exist: source nodes where only source ends coincide, sink nodes where only sink ends coincide, and mixed nodes where both source and sink ends coincide. The mixed nodes of a connector are internal to the connector and not accessible for external data exchange. The source and sink nodes of a connector, collectively called its boundary nodes or ports, are used to connect to (the ports of) components to exchange data. A source node atomically replicates an incoming data items into all of its coincident channel ends, whenever they are all ready to accept. A sink node nondeterministically selects a data item out of one of its coincident channel ends and delivers it as its outgoing data item, leaving all other data items in its coincident channels intact. The behavior of a mixed node is an atomic combination of the behavior of a source node and that of a sink node: whenever all of its coincident source channels ends are ready to accept data items, it selects a data item out of one of its nondeterministically chosen coincident sink channel ends, and atomically replicates it into all of its source channel ends.

A Sync channel has a source and a sink end. It accepts data from its source iff its sink can dispense it simultaneously. A LossySync has a source and a sink end. It reads a data item from its source and writes it simultaneously to its sink. If the sink end is not ready to accept the data item, the channel loses it. A SyncDrain has two source ends and no sink end. It reads data from its two ends and discards it iff the ends are ready to interact simultaneously. A \({FIFO_1}\) has a source end, a sink end, and capacity for only one data item. If it is empty, the channel accepts a data item from its source end and buffers it. If it is full, it is ready to dispense data through its sink end. Both ends of the channel cannot interact simultaneously. In addition to the primitive nodes, Merger and Replicator, here we use Router and Cross-product, which are shortcuts for derived connectors. The Reo nodes used in this work are explained as follows: A Replicator has one source end and one or more sink ends. It replicates data coming from its source to its sinks simultaneously. A Merger has one or more source ends and one sink end. It chooses one of its ready to interat source ends non-deterministically, receives a data item through this end, and writes it to its sink end simultaneously. A Router has one source end and a number of sink ends. It accepts a data item from its source and simultaneously replicates it on one of its non-deterministically chosen sink, which is ready to accept data. A Cross-product has a number of source ends and a sink end. It accepts a data item from each source, forms a tuple of them in the counter-clock-wise order with respect to its sink, where it writes the tuple, simultaneously.

3 Priority Flow

Here we define four channels to deal with priority in Reo.

A PrioritySync channel is similar to a Sync channel except it imposes priority on its flow, which propagates through the connector (unless it is blocked), and it can influence the non-deterministic choices in the containing connector by favoring data-flow alternatives that incorporate its ends. A BlockSourceSync channel is a Sync channel that blocks the propagation of priority from its source end towards its sink end. A BlockSinkSync channel is a Sync channel that stops propagation of priority from its sink end towards its source end. A BlockSync channel , a combination of BlockSourceSync and BlockSinkSync, stops the propagation of priority in both ways.

We model priority using the concepts of innate and acquired priority. Both ends of priority sync have innate priority. When an end with innate priority connects to another end that has no priority, the new end will obtain acquired priority. When one end of a synchronous type channel (e.g., sync, lossy sync, sync drain, ...) has acquired priority, the other end has innate priority.

However, in the case of non-synchronous channels (e.g., FIFO, async drain) and also the priority blocking channels, their ends can only have acquired priority. We update the constraint-based framework for Reo [16] to capture priority and the priority propagation mechanism, which we informally described above. In the rest of this paper, we omit data constraints when defining behavior of Reo elements. Data constraints are irrelevant for priority flow and were thoroughly covered in [16]. Motivated by the constraint-based nature of Reo itself, and the fact that constraint solving has advanced to the point that a number of practically useful constraint solvers exist today that can cope with realistically sized problems, we propose to define the behavior of Reo channels, as algebraic constraints that alter a set of variables.

Fig. 1.
figure 1

7-Sequencer

Full size image

Let \(\mathcal {N}\) and \(\mathcal {M}\) be global sets of ends and state memory variables, respectively. A free variable v has one of the following forms, where \(n \in \mathcal {N}\) and \(m \in \mathcal {M}\): \(\tilde{n} \in \{ \top , \bot \}\) shows presence or absence of data-flow on n; \(\mathring{m}, \mathring{m}' \in \{ \top , \bot \}\) denotes whether or not the state memory variable m is defined in the source and the target states of the transition, respectively; \(n^\triangleright \in \{ \top , \bot \}\) indicates the reason for lack of data-flow on n originating from the primitive or the context (of this primitive), respectively; \(n^{!^\bullet }\), \(n^{!^\circ } \in \{ \top , \bot \}\) models priority flow denoting whether n has acquired or innate priority. An end n has priority iff \(n^{!^\bullet } \vee n^{!^\circ } = \top \).

A constraint \(\varPsi \), which encodes the behavior of a Reo network is defined as: \(a {:}{:}= \tilde{n}\ |\ n^{!^\bullet }\ |\ n^{!^\circ }\ | \ n^\triangleright \ |\ \mathring{m}\ |\ \mathring{m}'\) (atoms), (formulae) A solution to is a map from the variable sets V to a value in \(\{\bot , \top \}\). The satisfaction rules for a solution \(\langle \delta \rangle \) are satisfaction in propositional logic. We denote the set of all solutions for \(\varPsi \) as \(\mathfrak {S}(\varPsi )\).

Definition 1 (RCSP)

A Reo Constraint Satisfaction Problem (RCSP) is a tuple \(\langle \mathcal {N}, \mathcal {M}, M_0, \mathcal {V}, C \rangle \), where: \(\mathcal {N}\) is a finite set of ends. \(\mathcal {M}\) is a finite set of state memory variables. \(M_0 \subseteq \mathcal {M}\) is a set of state memory variables that define the initial configuration of a network. \(\mathcal {V}\) is a set of variables v defined by the grammar \(v {:}{:}= \tilde{n}\ |\ n^\triangleright \ |\ \mathring{m}\ |\ \mathring{m}'\ |\ n^{!^\circ }\ |\ n^{!^\bullet }\ \text {for}\ n \in \mathcal {N}\ \text {and}\ m \in \mathcal {M}.\) \(C=\{C_1,\ C_2,\ ...,\ C_m\}\) is a finite set of constraints, where each \(C_i\) is a constraint given by the grammar \(\varPsi \) involving a subset of variables \(V_i \subseteq \mathcal {V}\).

Definition 2

(Composition \(\odot \)). The composition of two RCSPs \(\rho _1=\langle \mathcal {N}_1,\) \(\mathcal {M}_1,\) \(M_{0,1},\ \mathcal {V}_1,\ C_1 \rangle \) and \(\rho _2=\langle \mathcal {N}_2,\ \mathcal {M}_2,\ M_{0,2},\ \mathcal {V}_2,\ C_2 \rangle \) is defined as follows: \(\rho _1 \odot \rho _2=\langle \mathcal {N}_1 \cup \mathcal {N}_2,\ \mathcal {M}_1 \cup \mathcal {M}_2,\ M_{0,1} \cup M_{0,2},\ \mathcal {V}_1 \cup \mathcal {V}_2,\ C_1 \wedge C_2 \rangle \).

Axiom 1 (Join axiom)

To propagate no-flow reasons, when a source end c and a sink end k from two networks, the following holds: \( \lnot \tilde{c} \Leftrightarrow \lnot \tilde{k} \Leftrightarrow ({c}^\triangleright \vee {k}^\triangleright ).\)

Axiom 2 (Priority join axiom)

When a source end c and a sink end k from two networks connect, this holds: \((c^{!^\circ }\vee c^{!^\bullet } \Leftrightarrow k^{!^\circ }\vee k^{!^\bullet }) \wedge (c^{!^\circ }\wedge k^{!^\circ } \Leftrightarrow c^{!^\bullet }\vee k^{!^\bullet }).\)

Axiom 3 (Non-deterministic choice axiom)

Let N be a set of ends from which a Reo primitive chooses one for communication non-deterministically. The following guarantees that a node y with no priority has flow only if no prioritized node, e.g., x, is ready to interact: \((\lnot \tilde{x} \wedge (x^{!^\circ }\ \vee \ x^{!^\bullet }) \wedge \tilde{y} \wedge \lnot (y^{!^\circ }\ \vee \ y^{!^\bullet })) \Rightarrow \lnot x^\triangleright \)

In [16], the authors described the constraints that a primitive imposes on a network as a CSP. We extend these constraints with priority capturing variables. If the variable \(p^{!^\bullet }\) is true, the end p has innate priority. For example, in a PrioritySync channel, both ends have innate priority. A primitive end can also obtain innate priority via propagation. For instance, if one end of a Sync channel has acquired priority, which means it is prioritized because a primitive connected to it propagates priority, then the other end will have innate priority. We denote acquired priority for a primitive end p as: \(p^{!^\circ } \wedge \lnot p^{!^\bullet }\). The priority capturing constraint for a Sync channel with source end a and sink end b can be specified as follows: \(\lnot (a^{!^\circ } \vee a^{!^\bullet } \vee b^{!^\circ } \vee b^{!^\bullet }) \vee (a^{!^\circ } \wedge \lnot a^{!^\bullet } \wedge b^{!^\bullet }) \vee (a^{!^\bullet } \wedge b^{!^\circ } \wedge \lnot b^{!^\bullet })\). The assertion \(\lnot p^{!^\bullet }\) blocks the priority propagation on p. Though, p can still have acquired priority through a potential connecting primitive when \(p^{!^\circ } = \top \).

figure m

Table 1 shows the constraint encoding of Reo channels and nodes in presence of priority flow. The solutions to the CSP expressing the behavior of a Reo network encode possible data-flow through its nodes. Since a network may later connect to another network, the constraints should account for priority imposed by potential future connections. This information can be discarded when analyzing the behavior of a network in isolation. To exclude such cases, we should restrict the possible values of boundary ends.

Axiom 4 (Grounding axiom)

Let \(B \subset N\) be the set of boundary nodes in a Reo network. We rule out the solutions that are only present for further expansion of the network by: \(\forall b \in B: b^{!^\circ }\Rightarrow b^{!^\bullet }.\)

Solutions of the RCSP represent semantics of the corresponding Reo network, but they are specified as equations, which are much harder to interpret than an equivalent automata-based semantics. To tackle this issue, we introduce a new form of automata-like semantics for Reo, which we call Reo Labeled Transition System (RLTS). The purpose of the RLTS is to compactly represent solutions of RCSPs for visualization, model checking and simulation. Given a Reo network, its RCSP can be obtained by traversing the network and forming the conjunction the constraint encodings of its primitives. The procedure to solve an RCSP is presented in Algorithm 1. It takes a Reo connector and its RCSP and outputs the solutions set and the initial state of the connector. First, the algorithm initializes the global variables that keep the states of FIFO channels (fifoStates), the states to explore (toExplore), and the visited states (visited) (lines 2,3). While toExplore is not empty, \(\varPsi \) is updated with the current state and its conjunctive normal form (CNF) is produced for computing the solutions of the Boolean predicates (lines 4,5). The \(\langle state' \rangle \) indicates the new state of the connector and if it is not already explored or queued to be processed, it gets added to the list of states to be explored (lines 6–9). Then, the solutions set is updated with the current solution (line 13). The final output is the set of solutions and the initial state.

Table 1. Constraint encoding of Reo with priority
Full size table
Table 2. Updating Priority capturing constraints
Full size table

Definition 3 (RLTS)

A Reo Labeled Transition System (RLTS) is a tuple \(\mathcal {RLTS}\) \(=\) \((\) \(\mathcal {N},\ \mathcal {M},\ \) \(Q,\ \) \(\rightarrow ,\ \) \(q_0)\), where: \(\mathcal {N}\) is a set of ends, \(\mathcal {M}\) is a set of state memory variables, Q is a (finite) set of states of the form \(\langle M \rangle \), M is the set of state memory variables that are valid in the given state, \(\mathord {\rightarrow } \subseteq Q \times 2^{\mathcal {N}} \times 2^{\mathcal {N}} \times 2^{\mathcal {N}} \times Q\) is a transition relation, wherein N, R, and I in \((q,\ N,\ R,\ I,\ p) \in \rightarrow \) represent the ends that have flow, those without flow for which the reason for no flow is the end not being ready for interaction, and the ends with priority. Note that \(n \not \in N\) does not always mean \(n \in R\) as the reason for data flow can be the network (then, n requires a reason for no flow). \(q_0 \in Q\) is the initial state. We write \(q\xrightarrow {N,\ R,\ I}p\) instead of \((q,\ \) \(N,\ \) \(R,\ \) \(I,\ \) \(p)\) \(\in \) \(\mathord {\rightarrow }\). For \(n \in I, n \notin R \Leftrightarrow n \in N\).

Definition 4

(Composition \(\boxdot \)). We define the composition of \(L_1=(\mathfrak {N}_1,\ \mathcal {M}_1,\ \) \( Q_{1},\) \(\rightarrow _1,\ q_{0_1})\) and \(L_2=(\mathfrak {N}_2,\ \mathcal {M}_2,\ Q_{2},\ \rightarrow _2,\ q_{0_2})\) as: \(L_1\boxdot L_2=(\mathcal {N}_1\cup \mathcal {N}_2,\ \mathcal {M}_1 \cup \mathcal {M}_2,\ \rightarrow ,\ q_{0_1}\times q_{0_2})\) where \(\rightarrow \) is defined as:

figure n
figure o

We define few operations on a solution s for \(\varPsi =\langle \mathcal {N}_{\varPsi },\) \(\mathcal {M}_{\varPsi },\) \(M_{\varPsi 0},\ \) \(\mathcal {V}_{\varPsi },\ \) \(C_{\varPsi }\) \(\rangle \): source(s)=\(\langle \{m|m^\circ \in \mathcal {M}_{\varPsi }: s(m^\circ )=\top \}\rangle \), target(s)=\(\langle \{m|m'^\circ \in \mathcal {M}_{\varPsi } : s(m'^\circ )=\top \}\rangle \), flow(s)=\(\{n|n\in \mathcal {N}_{\varPsi }\): \(s(\tilde{n})=\top \}\), reason-giving(s)=\(\{n|n\in \mathcal {N}_{\varPsi }: s(n^\triangleright )=\top \}\), priority(s)=\(\{n|n\in \mathcal {N}_{\varPsi }: (s(n^{!^\circ }) \vee s(n^{!^\bullet }))=\top \}\). We say , where q = source(s), N = flow(s), R=reason-giving(s), I = priority(s), p = target(s).

Definition 5 (Visualization)

The visualization function \(\gamma \) on \(\varPsi =\langle \) \(\mathcal {N},\ \) \(\mathcal {M},\ \) \(M_{0},\ \) \(\mathcal {V}\), \(C\) \(\rangle \) yields \(\mathcal {L}\) \(=\) \((\) \(\mathcal {N},\ \) \(\mathcal {M},\) Q,  \(\rightarrow , \) \(q_0)\), where \(\mathcal {M}=\{m|s(m^\circ )=\top \vee s(m'^\circ )=\top , s\in \mathfrak {S}(\varPsi )\}\), \(Q=\bigcup _{s\in \mathfrak {S}(\varPsi )}\){source(s), target(s)}, \(\rightarrow =\) \(\{(source(s),\) flow(s),  \(\text {reason-giving}(s)\), \(\text {priority}(s)\), target(s)) \(|s\in \mathfrak {S}(\varPsi )\}\), \(q_0\) \(=source(s_0)\).

Theorem 1

Let \(\varPsi _{1}\) and \(\varPsi _{2}\) be two RCSPs, we show that \(\gamma (\varPsi _1 \odot \varPsi _2) = \gamma (\varPsi _1) \boxdot \gamma (\varPsi _2)\).

Proof

Let \(\gamma (\varPsi _1)\)=\((\mathfrak {N}_1,\) \(\mathcal {M}_1,\) \(Q_1,\ \) \(\rightarrow _1,\ q_{0_1})\), \(\gamma (\varPsi _2)= (\) \(\mathfrak {N}_2,\ \) \(\mathcal {M}_2,\) \(Q_2,\ \) \(\rightarrow _2,\ q_{0_2})\), and \(\gamma (\varPsi _1\ \odot \ \varPsi _2)=(\mathfrak {N},\ \) \(Q,\ \) \(\rightarrow ,\ q_{0})\). It is trivial to see that \(\mathfrak {N}=\mathfrak {N}_1 \cup \mathfrak {N}_2\), \(\mathcal {M}=\mathcal {M}_1 \cup \mathcal {M}_2\), \(Q=Q_1 \times Q_2\), \(q_0=q_{0_1} \times q_{0_2}\). Assume \(\exists s \in \mathfrak {S}(\varPsi _1 \odot \varPsi _2)\), \(s_1,\in \mathfrak {S}_1\), \(s_2 \in \mathfrak {S}_2\), , s.t. \(s_1 \backsim t_1\) and \(s_2 \backsim t_2\), but s.t. \(s \backsim t\). Therefore, \(N_1 \cap \mathfrak {N}_2 \ne N_2 \cap \mathfrak {N}_1 \wedge N_1 \cap \mathfrak {N}_2 \ne \emptyset \) or \((N_1\cup N_2)\cap (R_1\cup R_2)\ne \emptyset \). The latter is impossible. For the former, either \(n \in N_1, n \notin N_2\) or \(n \in N_2, n \notin N_1\), which is not possible as it means \(s(n)=\top \wedge s(n)=\bot \). Similarly, we can show it is impossible to have a t in \(\gamma (\varPsi _1 \odot \varPsi _2)\), when there is no \(s \in \mathfrak {S}\) s.t. \(s \backsim t\).

RLTS is comparable with Reo automata [12], a context-dependent formal semantic of Reo. A transition in Reo automata is labeled with a guard, which is a Boolean predicate in disjunctive normal form expressing positive and negative information about presence or absence of I/O requests, and a firing set that models the occurring I/O operations in the transition. The second set in RLTS transitions (the set of ends that provide reason for no flow) correspond to the negated elements of the guards in Reo automata, while the set of ends with flow relates to both the firing set and the positive elements of the guards. Unlike Reo automata, RLTS supports priority.

4 Numeric Priority

In BPMN, an error event has the highest priority, and the exception has priority over the normal flow. In this extension, the range for priority variables of an end n, \(n^{!^\circ }\) and \(n^{!^\bullet }\), is \(\mathbb {N}\) (natural numbers) \(\cup \) \(\{0\}\), where 0 indicates no priority. The larger number is the higher priority it represents. Each PrioritySync channel comes with a user defined priority value, which propagates through its ends. To propagation of a higher priority over a lower priority or no priority, we constrain priority variables to be greater than or equal to their initial values. Table 2 shows the priority related parts of the Reo constructs constraints. \(\langle \delta \rangle \vDash x \ge P \) iff \(\delta (x)\ge P\), \(\langle \delta \rangle \vDash x>P \) iff \(\delta (x)> P\), \(\langle \delta \rangle \vDash x=P \) iff \(\delta (x)=P\), where \(x\in \{x^{!^\bullet }, x^{!^\circ }\}, P\in \mathbb {N}\cup \{0\}\). The new constraint-based encodings of the replicator and router nodes in this table are constructed in accordance with Axiom 3.

Definition 6 (NPRLTS)

A Numeric Priority Reo Labeled Transition System is a tuple (\(\mathcal {N},\ \mathcal {M},\ Q,\ \rightarrow ,\ q_0\)), where: \(\mathcal {N}\) is a set of ends, \(\mathcal {M}\) is a set of state memory variables, Q is a (finite) set of states of the form \(\langle M \rangle \), M is the set of state memory variables that are valid in the given state, \(\mathord {\rightarrow } \subseteq Q\times 2^{\mathcal {N}}\times 2^{\mathcal {N}} \times \mathcal {N}\mapsto \mathbb {N} \times Q\) is a transition relation, wherein N, R, and \(f_I\) in \((q,\ N,\ R,\ f_I,\ p) \in \rightarrow \) are the ends having flow, those without flow for which the reason for no flow is the end not being ready for interaction, and a partial map of nodes with priority to their priority values, respectively. \(q_0 \in Q\) is the initial state. We write \(q\xrightarrow {N,R,f_I}p\) instead of \((q,\ N,\ R,\ f_I,\ p)\) \(\in \) \(\mathord {\rightarrow }\). For all \(q\xrightarrow {N,R,f_I}p\): \(f(n) > 0, n \notin N \Leftrightarrow n \in R\). We redefine priority(s) as \(\{(n, p)|n\in \mathcal {N}_{\varPsi }: s(n^{!^\circ })=p \vee s(n^{!^\bullet })=p\}\).

Definition 7 (Extended Visualization)

The visualization function \(\gamma \) on \(\varPsi =\langle \mathcal {N}_{\varPsi },\ \mathcal {M}_{\varPsi },\ M_{\varPsi _{0}},\ \mathcal {V},\ C\rangle \) yields \(\mathcal {L}=(\mathcal {N}_L,\ \mathcal {M}_L,\ Q, \ \rightarrow ,\ q_0)\), where \(\mathcal {N}_L=\{n|s(\tilde{n})=\top , \ s\in \mathfrak {S}(\varPsi )\}\), \(\mathcal {M}_L=\{m|s(m^\circ )=\top \ \vee \ s(m'^\circ )=\top , \ s\in \mathfrak {S}(\varPsi )\}\), \(Q=\bigcup _{s\in \mathfrak {S}(\varPsi )}\){source(s), target(s)}, \(\rightarrow =\) \(\{(source(s),\) flow(s),  reason-giving(s), \(\text {priority}(s)\), \(target(s))\ \) \(|\ s\in \mathfrak {S}(\varPsi )\}\), \(q_0\)=\(source(s_0)\).

5 Case Study

Here we demonstrate the application of our approach via an example and present a performance evaluation of our approach. Figure 2(a) depicts a sales process, which starts by receiving an order. It proceeds by reserving the ordered items for the customer. Then, the customer gets charged and her account is updated. Meanwhile if the payment encounters a problem, a cancellation event is triggered, which causes compensation for all of the performed activities. However, if an error event occurs, all tasks inside the transaction stop, the boundary error catch event redirects the flow to notifying the operator. Finally, if no problem occurs, the ordered items are shipped and the process ends.

Figure 2(c) shows a Reo network that simulates this process. The process starts by reading a token from the writer \(W_2\), which resembles receiving an order. Though a Reo network can be used for modeling infinite data flow, in the BPMN standard, when a start event is triggered, a new instance of the process is instantiated. Therefore, the Reo network is designed to handle only one request. The end \(A_1\) reads a token from the writer \({W_2}\) and directs it to replicator node B, which duplicates the token and forwards them to the BC and BE \({FIFO_1}\) channels. The token from BC continues to the CD \({FIFO_1}\) channel. If the payment succeeds, the flow from CD and BE \({FIFO_1}\) channels merge and a token enters the FG \({FIFO_1}\) channel. Then, it gets consumed by the reader \(R_3\).

If the payment fails, performed activities need to be compensated. A token from \(W_1\) simulates a payment failure, so the process needs to be canceled. The prioritySync channel IJ imposes a priority of one on the failure associated flow. The node J replicates the failure token into the lossySync channels JM and JU, depending on whether each of the \({FIFO_1}\) channels BC and CD is empty or full, the connected lossySync channels lose the incoming tokens or pass them to the adjacent syncDrain to consume the tokens of \({FIFO_1}\) channels, respectively. At the same time, the replicator node J writes into the \({FIFO_1}\) channels JK and JN, which simulate cancel reservation and undo changes tasks, respectively. The flow corresponding to error, starting from the writer \(W_3\), is structurally similar to the failure flow, but it has a priority of 2 due to SQ PrioritySync.

To analyze the presented BPMN process, we convert it to a Reo network. The core mapping is presented in [7, 17], which maps a task to a \({FIFO_1}\) channel, while it converts message, cancel, and error events to writer components simulating the incoming flows from the environment. A diverging parallel gateway is mapped to a replicator, while a converging parallel gateway is mapped to a join. The sequence flows are converted into sync channels. The mapping of exception and error handling flows are more complex and are presented in [27].

In this example, the error handling flow has the highest priority, while the exception handling has the medium priority, and the success flow has no priority. The choice between these three alternative flows is made by the routers. We obtain the NPRLTS as follows: First, we form the RCSP of the network by traversing through its primitives. Then, we solve the obtained RCSP and extract transitions from obtained solutions, as described in Algorithm 1.

To show the effect of priority on our example, we first investigate the behavior of the network in absence of priority, wherein the normal flow of the process can continue even in case of a payment failure. This is because the router node E chooses one of its outgoing flows non-deterministically. The following assets a priority-respecting routing of these alternative flows. \((\{BE\} \in source(t) \wedge (C_1 \in flow(t) \vee E_1 \in flow(t))) \Rightarrow ((W_3 \notin \) \(reason-giving(t) \Leftrightarrow W_3 \in flow(t)) \wedge (W_3 \in reason-giving(t) \wedge W_1 \notin reason-giving(t)) \Leftrightarrow W_1 \in flow(t))\).

A typical way of verifying this property is to check it against the NPRLTS of the network. The given property is straight forward to check. Due to the number of ends in this example, the transition labels of the NPRLTS are lengthy. Thus for brevity, we apply an abstraction on the original NPRLTS, which leads to a more concise and readable model. To address a node end, we append a number index to the node name (e.g., \(B_1\)). We refer to a channel using the name of the nodes connected to its ends (e.g., BC). Similarly, we append a number index to a channel name to denote a channel end (e.g., \(BC_1\)). In addition, we group the ends with a similar name e.g., \(B_{1,2}\) (referring to ends \(B_1\) and \(B_2\)).

Since, the property solely mentions the ends \(C_1\), \(E_1\), \(W_1\), and \(W_3\) on the transitions originating from the states where BE \({FIFO_1}\) channel is full, we abstract from the rest of the ends in those transitions and from all the ends in other transitions. It is straight-forward to see that this abstraction does not affect the correctness of the validation due to the nature of the property.

Figure 2(b) shows the abstract NPRLTS of the network of Fig. 2(c) in absence of priority. The property that we are interested to check is that if from any state wherein BE holds, \(W_3\) has flow unless it provides a reason for no flow itself, and if \(W_3\) provides a reason for no flow, \(W_1\) has flow unless it provides a reason for no flow itself. This property, however, does not hold on the current NPRLTS as it contains transitions originating from states \(\{BC, BE\}\) and \(\{CD, BE\}\), wherein either \(W_3\) is absent in R (the set of ends providing a reason for now flow), yet it is not in N (the set of ends with data flow) or \(W_3\) is in R, but \(W_1\) is not in R, yet it is not in N.

Here we show how considering priority constraints rules out these transitions. We reason about one of the transitions (the transition from \(\{BC, BE\}\) to \(\{CD, BE\}\) with \(N=\{C_1,...\},\) \(R=\{W_1,...\}\)). Similar reasonings hold for the rest.

figure p

This disproves the existence of the aforementioned transition meaning that when \(\{BC\}\) and \(\{BE\}\) are full, the request from \(W_1\) is not ignored.

Fig. 2.
figure 2

Performance evaluation of N-Sequencers

Full size image
figure q

The execution time of the Algorithm 1 depends on the number of states of the RCSP and the time to solve the RCSP. Thus, to study the performance of our framework and to compare it with the existing approaches, we choose N-Sequencer, which consists of N FIFO channels that are circularly connected. Adding each \({FIFO_1}\) channel doubles the number of states in the corresponding semantic model and increases the complexity of the constraints encoding the behavior of the network by adding new variables and new assertions on them. This makes the network a good choice for our benchmarking, where we would like to compare the solutions on state explosion. Since we are interested in comparing our approach with the existing tools, we do not include priority in our case study. This is justified by the fact that incorporating priority does not affect the number of states in the model and influences only the size of the constraint. In addition, adding more \({FIFO_1}\) channels to the network increases both the number of states and the size of the constraint capturing the semantics of the network. Since we use optimized third-library tools to solve the constraints, we do not distinguish between the various form of constraints obtained from different channels and instead we observe the approximate growth of the size of constraints.

Figure 1 shows a 7-sequencer. Though the size of the operational semantics model of this network grows in a linear fashion in relation with N, the number of intermediate states to compute the final results grows exponentially. The benchmarks have been performed on Mac Book Pro OS X El Capitan with 2.8 GHz Intel Core i7 and 16 GB MHz DDR3 memory. Our approach is implemented in Java 8. We have used Reduce Algebra System revision number 2337 to compute the conjunctive normal form of the constraints and to solve them. We have experimented with an optimization on the number of variables used in the constraints by substituting equal variables with a single variable. Figure 2(a) presents the average time to compute a single solution of the RCSP of an N-Sequencer. Figure 2(b) shows the relation between N and the size of the RCSP’s constraints of an N-Sequencer. This is an indication of the complexity of the constraint. Figure 2(c) illustrates the total time required to compute all solutions of a RCSP’s constraint of an N-Sequencer. Figure 2(d) shows the time consumed to calculate the coloring semantics and the constraint automata semantics of N-Sequencers using the ECT toolset. The computation of the coloring semantics and the constraint automata fail with the stack overflow error for \(N=16\) and \(N=21\), respectively. The results shows that our approach handles larger models than the existing tools can. The effect of the optimization is more significant for larger N.

6 Related Work

Several works, e.g., [10, 11, 22] use priorities to model scheduling policies. Many workflow languages rely on Petri nets [2, 4]. Priority flow in Petri net-based process models is managed with the help of inhibitor arcs and transition priorities [31]. Inhibitor arcs allow a transition to fire only if the adjacent place is empty. Prioritized Petri nets [9] introduce a partial order on transitions. Given a set of enabled transitions, the transitions with higher priority fire before the transitions with lower priority. Others, e.g., [28, 34] use a partial order on transitions to model priority. Our earlier approach in modeling priority using binary variables supports a limited form of priority compared to the mentioned Petri nets approaches. However, the proposed extension bridges this gap by defining priorities as non-zero natural numbers. An advantage of our model is its compositionality. Compared to the aforementioned methods, Reo fits in the realm of component-based or service-oriented architecture in a compositional way. Reo is an extensible language, where new behavioral aspects can be added. An effort to express the behavior of Reo networks via constraints is reported in [19]. It demonstrates the efficiency of the constraint-based approach. It models synchronization and data flow constraints, but no priority flow was considered. In [16], a framework is presented to encode semantics of Reo networks as CSP with predicates in the form of binary propositions and numerical constraints. An advantage of this method is handling data constraints symbolically and, hence, mitigating the state explosion problem of automata models. We extended this framework to handle priority constraints, taking a step forward toward implementing a toolset that covers all behavioral aspects of Reo. Among the formal semantics of Reo, connector coloring comes with a limited notion of priority based on the context information. The context information affects otherwise non-deterministic data-flow choices. In [26], an automata-based semantics is proposed, which associates a preference for each transitions. A transition of lower preference is fired iff no more preferred transition can occur.

7 Conclusions and Future Work

In this paper, we addressed the problem of priority flow modelling using the Reo coordination language. We extended the unified constraint-based semantics of Reo with binary and numeric priority constraints, showed correctness of our approach for the binary case and evaluated the performance of the algorithm for solving the RCSP to derive the semantics of a Reo network given the behavior of its consituent elements. We also illustrated the use of our framework for modeling business processes with priority flow.

As part of our ongoing work, we are using this framework to encode other aspects of the semantics of Reo, specifically, timed behavior. A promising area for future work is to use our framework for constraint-based model checking of Reo networks with priority.