Extending Paradigm with Data

Abstract

We discuss an extension of the coordination modeling language Paradigm. The extension is geared towards data-dependent interaction among components, where the coordination is influenced by possibly distributed data. The approach is illustrated by the well-known example of a bakery where tickets are issued to serve clients in order. Also, it is described how to encode Paradigm models with data in the process language of the mCRL2 toolset for further analysis of the coordination.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The so-called IWIM model for the coordination of concurrent components as proposed by Farhad Arbab and co-workers [3, 6] distinguishes ideal workers and ideal managers. Among others, IWIM forms the conceptual framework for the coordination language Manifold [4, 7]. The central ideas of IWIM evolved into the theory of Reo connectors [5], which exploits constraint automata for its semantics and whose distributed implementation approach separates coordination from parallelism [11].

Rather than considering hierarchies of components with atomic workers at the bottom layer and one overall manager at the top as for IWIM, the coordination modeling language Paradigm [9] takes networks of components as starting point, where each component exhibits both worker and manager activity. The worker activity is the internal behavior of the component that executes as local transitions asynchronously from other components; the manager activity consists of the synchronous interaction with other (groups of) components governed by so-called consistency rules. In terms of constraint automata, consistency rules comprise the atomic dataflow among synchronizing components. However, via a mechanism of phases and traps it is guaranteed that the local behavior, the worker level of a component, remains aligned with the global behavior, the manager level of the component.

In this paper an extension to Paradigm including data is proposed. In this extension, consistency rules incorporate the local variables of the components and expressions thereof, in particular to compare or communicate their value. So, our data extension will be geared towards interaction and coordination thereof. Cast in terms of Reo, the data constraints are enriched with data and values. For Paradigm with data, the local memory of components can be accessed (via their ports) at the coordination level. Consequently, the communicated data itself can be stored too. However, this requires that the phases-and-trap mechanism of Paradigm needs to be adapted, somewhat complicating the semantics. An encoding scheme for Paradigm, without data, into the model checking toolsuit mCRL2¹, as proposed in [1], brings the advantage of formal analysis of the coordination among components. For a concrete coordination problem, we will describe a Paradigm model with data of a bakery, describe its encoding in mCRL2’s specification language.

Outline Sect. 2 provides a formal definition of Paradigm with data and provides its operational semantics. Section 3 illustrates and further explains the underlying concepts for the case of a bakery where clients need to be served in order of arrival. Section 4 discusses how formal analysis of Paradigm using the mCRL2 toolset can be obtained. Section 5 wraps up the paper.

2 Formal Definitions

We subsequently introduce components with variables, Paradigm models and consistency rules with data, and configurations with local transitions and global transfers among them. An example illustrating the above notions is presented in the next section.

Definition 1

Let, for some index set I, a number of local variables $v_i$ of type $D_i$, respectively, be given. Put $E = \prod _{i{\in }I} \, D_i$. Furthermore, fix a set of actions A. For E and A, a Paradigm component C is a tuple $C = ( \varSigma , T, \varPsi )$ where

• (i) for some set S, the elements of which are called states, $\varSigma = S \times E$ is the set of extended states of C

• (ii) $T \subseteq \varSigma \times A \times \varSigma$ is the transition relation of C

• (iii) $\varPsi = ( \varPhi _1, \ldots , \varPhi _n )$, for some $n \geqslant 0$, is a tuple of partial functions, called the roles of C, where each $\varPhi : \mathcal {P}(T) \hookrightarrow \mathcal {P}(\mathcal {P}(\varSigma ))$ is such that if $\sigma \in \theta$, $\theta \in \varPhi (\varphi )$, and $\langle \sigma , a, \sigma ' \rangle \in \varphi$ then also $\sigma ' \in \theta$.

By definition, an extended state $\sigma \in \varSigma$ is a pair $\sigma = (s,e)$ of a state $s \in S$ and a tuple of ‘current’ values of the variables. We write $\sigma \xrightarrow {\,a\,} \sigma '$ for a transition in T, rather than $\langle \sigma , a, \sigma ' \rangle \in T$. For a role $\varPhi$, i.e. a coordinate of $\varPsi$, an element $\varphi$ of $\mathrm {dom}(\varPhi )$ is called a phase of $\varPhi$. An element $\theta$ of $\varPhi (\varphi )$ is called a trap of $\varphi$. The idea is, a transition, $\sigma \xrightarrow {\,a\,} \sigma '$ starting from an extended state $\sigma$ in a trap $\theta$ of a phase $\varphi$ say, does not move outside of the trap. Hence, it is required for such a transition $\sigma \xrightarrow {\,a\,} \sigma '$ that the extended state $\sigma '$ lies in $\theta$ too. So, in phase $\varphi$, once having entered $\theta$, control is trapped in $\theta$. The phases constituting $\mathrm {dom}(\varPhi )$ of a role $\varPhi$ will typically partially overlap, their overlaps being traps. One may think of a trap as a final stage within a phase. Reaching a trap of a phase indicates that a transfer to another phase is about to happen.

Suppose $\varphi _i \in \varPhi _i$, for $i = 1, \ldots , n$, for the roles $\varPhi _1, \ldots , \varPhi _n$ of component C, and suppose $\sigma \xrightarrow {\,a\,} \sigma '$ is a transition of C, i.e. an element of T, such that the transition $\sigma \xrightarrow {\,a\,} \sigma '$ is an element of each $\varphi _i$ too. Then the transition $\sigma \xrightarrow {\,a\,} \sigma '$ is called an admitted transition with respect to the phases $\varphi _1, \ldots , \varphi _n$.

Definition 2

• (a) A Paradigm model with data consists, for some index set H, of a tuple $( C_h )_{h \in H}$ of Paradigm components

  $$\begin{aligned} C_h = ( \, \varSigma _h , {T_h}, \varPsi _h\, ) \end{aligned}$$

  with their own local variables and actions, as well as extended states in $\varSigma _h$, transition relations $T_h$, and roles $\varPsi _h = ( \varPhi _{h,1}, \ldots , \varPhi _{h,n_h} )$, for $h \in H$.

• (b) A consistency rule $\gamma$ for $( C_h )_{h \in H}$ consists, for an index set R, of a tuple $( \, C_r(\varPhi _r) : \varphi _r(e_r) \xrightarrow {\,\theta _r\,} \varphi '_r(e'_r) \, )_{r \in R}$ where $\varPhi _r$ is a role of component $C_r$, $\varphi _r$ and $\varphi '_r$ are phases of $\varPhi _r$, $e_r$ and $e'_r$ are values for the variables of $C_r$, and $\theta _r$ is a trap of $\varphi _r$.

• (c) A set of consistency rules $\varGamma$ is called closed if for each rule $( \, C_r(\varPhi _r) : \varphi _r(e_r) \xrightarrow {\,\theta _r\,} \varphi '_r(e'_r) \, )_{r \in R}$ of $\varGamma$, if there exists, for some $r \in R$, a state $s_r$ of $C_r$ for which both $(s_r,e_r), (s_r,\bar{e}_r) \in \theta _r$, then $\varGamma$ contains, for some $\bar{e}'_r$, a rule $\bar{\gamma }$ of the form $( \, C_r(\varPhi _r) : \varphi _r(\bar{e}_r) \xrightarrow {\,\theta _r\,} \varphi '_r(\bar{e}'_r) \, )_{r \in R}$ as well.

For clarity we assume that different components have distinct names for states, variables, and actions, and hence distinct roles, phases, and traps. However, in a consistency rule, a component may have multiple occurrences, viz. in different roles. Also, a component may not be involved in a consistency rule at all. The rules are called consistency rules in Paradigm because the requirement of each $\theta _r$ to be a trap of phase $\varphi _r$ guarantees that the ‘coarse-grained’ rule can only be applied if consistent with the current ‘fine-grained’ local state of each component involved. The closedness condition on sets of rules will guarantee that global behavior, to be defined in a minute, cannot be essentially influenced by local behavior respecting the traps mentioned in a rule.

Next, we define the behavior of a Paradigm model, with intra-component behavior (a so-called local transition) affecting the extended state of a single component vs. inter-component behavior (a global transfer) exchanging values and changing phases based on a trap in some of the roles of a number of components.

Definition 3

Let $\varPi = ( C_h )_{h \in H}$ be a Paradigm model and let $\varGamma$ be a closed set of consistency rules for $\varPi$.

• (a) A configuration of $\varPi$ is a tuple $\langle s_h, e_h, \psi _h \rangle _{h {\in } H}$, where for each index $h \in H$, $(s_h,e_h)$ is an extended state of component $C_h$, and $\psi _h = ( \varphi _{h,1}, \ldots , \varphi _{h,{n_h}} )$ is a tuple of phases such that $\varphi _{h,i} \in \varPhi _{h,i}$, for $i = 1, \ldots , n_h$.

• (b) A local transition $\langle s_h, e_h, \psi _h \rangle _{h {\in } H} \xrightarrow {\,a\,} \langle s'_h, e'_h, \psi _h \rangle _{h {\in } H}$ of $\varPi$ is an admitted transition of one of the components of $\varPi$, i.e. for some $h_0 \in H$ it holds that (i) $\langle s_{h_0}, e_{h_0} \rangle \xrightarrow {\,a\,} \langle s'_{h_0}, e'_{h_0} \rangle$ is an admitted transition for component $C_{h_o}$ with respect to the phases $\psi _{h_0} = ( \varphi _{h_0,1}, \ldots , \varphi _{h_0,n_{h_0}} )$, and (ii) $s_h = s'_h$ and $e_h = e'_h$ for each index $h \ne h_0$ in H.

• (c) A global transfer $\langle s_h, e_h, \psi _h \rangle _{h {\in } H} \xrightarrow {\,\gamma \,} \langle s_h, e'_h, \psi '_h \rangle _{h {\in } H}$ of $\varPi$ based on a consistency rule $\gamma = ( \, \hat{C}_r(\varPhi _r) : \varphi _r(\hat{e}_r) \xrightarrow {\,\theta _r\,} \varphi '_r(\hat{e}_h) \, )_{r \in R}$ updates phases and values as prescribed by $\gamma$, i.e. (i) if, for $h \in H$, $i = 1, \ldots , n_h$, it holds that $C_h = \hat{C}_r$ and $\varPhi _{h,i} = \varPhi _r$, for some index $r \in R$, then $(s_h,e_h) \in \theta _r$, $e_h = \hat{e}_r$ and $e'_h = \hat{e}_r$, $\varphi _{h,i} = \varphi _r$ and $\varphi '_{h,i} = \varphi '_r$, and (ii) if, for $h \in H$, $C_h \ne \hat{C}_r$ for each $r \in R$ then $e_h = e'_h$, and, for $h \in H$, $i = 1, \ldots , n_h$, $\varPhi _{h,i} \ne \varPhi _r$ for each $r \in R$ then $\varphi _{h,i} = \varphi '_{h,i}$.

A configuration $\langle s_h, e_h, \psi _h \rangle _{h {\in } H}$ of a Paradigm model $\varPi = ( C_h )_{h \in H}$ holds for each component $C_h$ the current extended state $(s_h,e_h)$ as well as the current phase $\varphi _{h,i}$ for each role $\varPhi _{h,i}$ of $C_h$.

Note, in a local transition $\langle s_h, e_h, \psi _h \rangle _{h {\in } H} \xrightarrow {\,a\,} \langle s'_h, e'_h, \psi _h \rangle _{h {\in } H}$, say for component $C_{h_0}$, component $C_{h_0}$ nor any of the other components changes phase; the tuple of phases $\psi _h$ is for each component the same in the source configuration $\langle s_h, e_h, \psi _h \rangle _{h {\in } H}$ and the target configuration $\langle s'_h, e'_h, \psi _h \rangle _{h {\in } H}$ of the transition. However, the transition must be admitted for $C_{h_0}$, i.e. it must be present in all of the phases $\varphi _{h_0,i}$ of $\psi _{h_0}$ for component $C_{h_0}$.

For a global transfer based on a consistency rule $\gamma$ to apply, the current phases $\varphi _{h,i}$ of role $\varPhi _{h,i}$ must match the phases of $\varPhi _r$, if $C_h = \hat{C}_r$ and $\varPhi _{h,i} = \varPhi _r$. Also, the extended states of the components $\hat{C}_r$ involved must lie in the traps $\theta _r$, for all $r \in R$. States remain unaffected, but values of variables may change for the components mentioned in the rule, presumably because of the interaction. Phases may change too for the components mentioned, from $\varphi _{h,i} = \varphi _r$ to $\varphi _{h,i} = \varphi '_r$, which are both phases within the role $\varPhi _{h,i} = \varPhi _r$. Components $C_h$ and phases $\varphi _{h,i}$ not mentioned by consistency rule $\gamma$ remain the same.

We have the following result.

Theorem 1

Let $\varPi = ( C_h )_{h \in H}$ be a Paradigm model, and let $\varGamma$ be a closed set of consistency rules for $\varPi$. Suppose

$$\begin{aligned} \langle s_h, e_h, \psi _h \rangle _{h {\in } H} \xrightarrow {\,\gamma \,} \langle s_h, e'_h, \psi '_h \rangle _{h {\in } H} \quad \text {and} \quad \langle s_h, e_h, \psi _h \rangle _{h {\in } H} \xrightarrow {\,a\,} \langle s'_h, e''_h, \psi _h \rangle _{h {\in } H} \end{aligned}$$

for configurations $\langle s_h, e_h, \psi _h \rangle _{h {\in } H}$, $\langle s_h, e'_h, \psi '_h \rangle _{h {\in } H}$, and $\langle s'_h, e''_h, \psi _h \rangle _{h {\in } H}$ of $\varPi$, a consistency rule $\gamma$ in $\varGamma$, and a local transition for a. Then also

$$\begin{aligned} \langle s_h, e_h, \psi _h \rangle _{h {\in } H} \xrightarrow {\,\gamma \,} \langle s_h, \bar{e}'_h, \psi '_h \rangle _{h {\in } H} \end{aligned}$$

for suitable values $\bar{e}'_h$, for $h \in H$.

The theorem is a direct consequence of the closedness condition for the set of consistency rules. It states that the execution of a local transition cannot disable the execution of a consistency rule. This is the loose coupling in Paradigm between the interaction between components and actions of the components of their own. The reverse obviously doesn’t hold. A local transition that was admitted before, may be forbidden by one of the phases put in place by the execution of a consistency rule. Care has to be taken to deal with variables that are set by local transitions as well as by global transfer. To ensure non-interference of the global (manager) and local (worker) level, one may want to restrict reading or updating of variables to happen outside of the traps involved in consistency rules that may change the value of the different variables.

3 An Example Paradigm Model

We illustrate the formal definitions of the previous section by modeling in Paradigm with data the handling of clients in a busy bakery. Clients entering the shop take a ticket from a ticket dispenser and wait for their turn. The client having the ticket displayed is being served. The baker increments the display after having handled a client and next serves the clients holding the ticket with the new number.

3.1 STDs for the Components

We first model the basic behavior of the components by means of state-transition diagrams (STD).

Client processes are introduced by the state-transition diagram below. Each client carries an integer variable c to hold a ticket number. Initially c is set to 0. A client subsequently obtains a ticket from the ticket machine, action $\textit{getTicket}$, shows the ticket to the baker (action $\textit{showTicket}$), clarifies his or her wishes (action $\textit{clarify}$), and finally thanks the baker and leaves (action $\textit{thankLeave}$). Note, apart from initialization, there is no explicit assignment to variable c in the STD. Also, we don’t bother to distinguish multiple instances of the $\textit{Client}$ process. Incorporating another variable, $id$ say, holding the identity of a client would cater for this.

The ticket machine is modeled by the process $\textit{Machine}$ which has an integer variable m for the number of the ticket it dispenses. Starting from initial value 1 for m, the machine may provide a ticket with the current value of m while moving to state 1 (action $\textit{provide}$) and returns to state 0 on an increment of the value of m (action $\textit{incr}$). The $\textit{incr}$-action is decorated with an assignment, viz. the increment $m := m+1$ of variable m.

The $\textit{Baker}$ process models the workflow for the baker. Starting from the initial state 0, with initial value 0 for the integer variable b of the process, the process cycles through its four states. First the baker aims to increment the display (action $\textit{incrDisplay}$), next the baker welcomes the client holding the number displayed (action $\textit{welcome}$) and helps the client (action $\textit{help}$). The baker closes the cycle by some thanks and greetings (action $\textit{thankGreet}$). Note, also here no explicit assignments to the variable b are present; changes to b will come from the interaction with the $\textit{Display}$ process described below.

The $\textit{Display}$ process is similar to the $\textit{Machine}$ process. It switches between two states. The $\textit{Display}$ process holds an integer variable d, initially set to 1. However, here we have chosen not to have an update of the variable in the STD as we have for the machine. As variation, the display gets incremented in the interaction with the baker. This is captured by the consistency rules modeling the interplay of these two processes.

3.2 Roles of the Components

As discussed above, in Paradigm a component can have multiple roles. At the level of the roles the interaction with other components takes place. The phase-and-trap discipline of Paradigm ensures that STD and roles remain aligned during execution: a local transition cannot change the current phase or move out of a trap.

A $\textit{Client}$ process has two roles, $\textit{NeedTicket}$ and $\textit{NeedService}$, in which it interacts with the $\textit{Machine}$ process and $\textit{Baker}$ process, respectively. The variable c of the $\textit{Client}$ process may be read and/or written during this interaction and is therefore displayed as parameter of the phases involved.

The role $\textit{NeedTicket}$ has two phases, $\textit{NotTaking}$ and $\textit{Taking}$. The phase $\textit{NotTaking}$ only allows the action $\textit{getTicket}$ modeling that a ticket needs to be obtained first. When state 1 is reached in the STD the trap $\textit{requestMachine}$ has been entered, signaling that in the role $\textit{NeedTicket}$ the component is prepared to leave phase $\textit{NotTaking}$ (and ready to enter phase $\textit{Taking}$, as we shall see). Phase $\textit{Taking}$ models a client in possession of a ticket. When state 2 has been reached, the trap $\textit{useDone}$ is entered. As required for a trap, the transitions for actions $\textit{clarify}$ and $\textit{thankLeave}$ do not leave trap $\textit{useDone}$.

The $\textit{Machine}$ process in its single role $\textit{GiveTicket}$ interacts with the $\textit{Client}$ processes in their roles $\textit{NeedTicket}$. The role $\textit{GiveTicket}$ has two phases, $\textit{Available}$ and $\textit{Unavailable}$, that manage the variable m, as indicated. Both phases have a single-state trap, trap $\textit{readyToProvide}$ for phase $\textit{Available}$, which indicates that a new ticket is available for issue when the trap is reached, and trap $\textit{providingDone}$ of phase $\textit{Unavailable}$, that indicates that the current ticket number has been issued and the variable m needs to be adapted (as it actually will be in phase $\textit{Available}$). Note, since variable m is updated when transition incr $[m := m+1]$ is taken, the consistency rule $(\text {CM}3)$ presented below doesn’t have an increment of its parameter.

The $\textit{Baker}$ process has two roles, role $\textit{NeedTurnNumber}$ for interaction with the $\textit{Display}$ process, and role $\textit{NeedNextClient}$ for interaction with all $\textit{Client}$ processes. Role $\textit{NeedTurnNumber}$ distinguishes the phases $\textit{NotUsing}$ and $\textit{Usage}$, that are connected by trap $\textit{requestNextNumber}$ from phase $\textit{NotUsing}$ to phase $\textit{Usage}$ and by trap $\textit{done}$ the other way around. The number of the client at turn is kept in the variable b of process $\textit{Baker}$.

When the $\textit{Baker}$ process needs to know the next ticket number to store it in its variable b, this is provided by the $\textit{Display}$ process, in its single role $\textit{ShowingNumber}$. In phase $\textit{Offering}$ the value of the variable d of process $\textit{Display}$ is guaranteed to be updated upon reaching trap $\textit{nextNumber}$. To enforce such an update, phase $\textit{Offering}$ is switched to phase $\textit{Passive}$, which will move control of $\textit{Display}$ to state 1 from which a next increment is possible once, and which is, via trap $\textit{ready}$, switched back to phase $\textit{Offering}$. Note, when changing phase from phase $\textit{Passive}$ to phase $\textit{Offering}$ as prescribed by consistency rule $(\text {BD}3)$, given in the next subsection, the variable d will be incremented. Different from the modeling of role $\textit{GiveTicket}$ of the $\textit{Machine}$ process presented above, the role $\textit{ShowingNumber}$ of the $\textit{Display}$ process doesn’t update the variable d itself.

The role $\textit{NeedService}$ of the $\textit{Client}$ process deals with the client-side in the interaction with the $\textit{Baker}$ process. The role has two phases, $\textit{NotServed}$ and $\textit{HavingTurn}$, each making use of the variable c of the $\textit{Client}$ process during interaction, viz. to match the ticket number announced by the baker. Only in case of a match, the $\textit{Client}$ process will change phase to $\textit{HavingTurn}$, based on the trap $\textit{requestBaker}$. To highlight, be it a bit sketchy, that traps aren’t necessarily comprised of a single state, the trap $\textit{ordered}$ of phase $\textit{HavingTurn}$ allows a transfer back to the phase $\textit{NotServed}$ again.

The role $\textit{NeedNextClient}$ of process $\textit{Baker}$ takes care of the baker’s part in the interaction with a client. When having reached trap $\textit{idle}$ in phase $\textit{FinishingHelp}$ (finishing helping a previous client), a transfer will take place (by consistency rule $(\text {BC}1)$ discussed below) to phase $\textit{StartingHelp}$. Similarly, in phase $\textit{StartingHelp}$ on reaching trap $\textit{started}$ a transfer will take place (now by consistency rule $(\text {BC}2)$) to phase $\textit{Helping}$, in which the client is actually served. After trap $\textit{ready}$ has been reached in phase $\textit{Helping}$, the $\textit{Baker}$ process will switch to phase $\textit{FinishingHelp}$ in role $\textit{NeedNextClient}$.

3.3 Interactions Among Components

The interaction between the $\textit{Client}$ processes, in their roles $\textit{NeedTicket}$, and the $\textit{Machine}$ process, in its role $\textit{GiveTicket}$, arranges that every client entering the bakery is provided with a uniquely numbered ticket. The three consistency rules $(\text {CM}1)$, $(\text {CM}2)$, and $(\text {CM}3)$ below describe how phases change once proper traps have been entered.

The first consistency rule, rule $(\text {CM}1)$, is a synchronous transfer of phases, as indicated by the $\otimes$-symbol and enclosing braces. Given that (i) the $\textit{Client}$ process, in role $\textit{NeedTicket}$, has reached trap $\textit{requestMachine}$ of phase $\textit{NotTaking}$, while (ii) the $\textit{Machine}$ process, in role $\textit{GiveTicket}$ resides in trap $\textit{readyToProvide}$ of phase Available, then (i) the $\textit{Client}$ process switches to phase $\textit{Taking}$ of role $\textit{NeedTicket}$, while (ii) the $\textit{Machine}$ process simultaneously changes to phase $\textit{Unavailable}$ of role $\textit{GiveTicket}$. Moreover, (i) the $\textit{Client}$ process is assumed to (still) hold the initial value 0, while (ii) the $\textit{Machine}$ process has with a (presumably fresh) ticket number n, then the value n is copied from the $\textit{Machine}$ process to the $\textit{Client}$ process. For consistency rules $(\text {CM}2)$ and $(\text {CM}3)$ the $\textit{Client}$ and $\textit{Machine}$ process act independently. Based on $(\text {CM}2)$, the $\textit{Client}$ process can change phase, from $\textit{Taking}$ to $\textit{NotTaking}$, via trap $\textit{useDone}$. Based on $(\text {CM}3)$, the $\textit{Machine}$ process can change phase, from $\textit{Unavailable}$ to $\textit{Available}$, via trap $\textit{providingDone}$.

The interaction between the $\textit{Baker}$ and $\textit{Display}$ process is governed by the three consistency rules $(\text {BD}1)$, $(\text {BD}2)$, and $(\text {BD}3)$. A similar effect is achieved as for rules $(\text {CM}1)$ through $(\text {CM}3)$. However, the actual update of variable m is done for the $\textit{Machine}$ process at the STD-level by the transition from state 1 to state 0 executing action $\textit{incr}[m := m+1]$. Here, for process $\textit{Display}$ the update is accomplished at the level of role $\textit{ShowingNumber}$ by rule $(\text {BD}3)$, which passes the parameter value m for phase $\textit{Passive}$ to phase $\textit{Offering}$ as parameter value $m+1$.

The interaction of the $\textit{Baker}$ and $\textit{Client}$ processes in their respective roles $\textit{NeedNextClient}$ and $\textit{NeedService}$ is more tied up compared to the interactions described above. All three consistency rules $(\text {BC}1)$, $(\text {BC}2)$, and $(\text {BC}3)$ prescribe simultaneous phase transfer for the two processes. Moreover, the value of the variable b of the $\textit{Baker}$ process must be equal to the variable c of the $\textit{Client}$ process; they must both have the value n.

4 Model Checking Paradigm Models with Data

As for many modeling languages, formal analysis of Paradigm models supports the modeling itself. In [1, 2] it is discussed how to expressing Paradigm models without data in the process language of the mCRL2 toolset [8, 10]. In short, for each component the local behavior is modeled as a state machine. For a transition to fire, it is checked if the current phase allows so. For the global behavior of a component a communication intent is issued for each consistency rule that mentions the component. However, the current state and phase should match the relevant trap. Correct interaction can subsequently be enforced by the allow and communication operators of mCRL2, that block single-sided communication intents and synchronize consistent ones, respectively. In this section, we describe by example how the approach extends to deal with data.

Fig. 1.

mCRL2 code for the $\textit{Client}$ process

Figure 1 provides the mCRL2 version of the process $\textit{Client}$ of the bakery example of the previous section (the complete code can be found in the appendix). Here, the Client process has four parameters, viz. the natural number st to hold the state of the underlying STD, the natural number c to hold the ticket number of the client, and the parameters nt_ph and ns_ph to keep track of the phase of the process with respect to their roles $\textit{NeedTicket}$ and $\textit{NeedService}$, respectively. For this, the definition of the two enumerated types

are included at the beginning of the specification. The specification of the Client process falls into three parts: (i) lines 3–10, specifying the local transitions (ii) lines 12–17, describing $\textit{Client}$’s part for the consistency rules $(\text {CM}1)-(\text {CM}3)$, and similarly (iii) lines 19–27 for the consistency rules $(\text {BC}1)-(\text {BC}3)$. Each part consists of a number of alternative branches, separated by the non-deterministic choice operation ‘+’, of the form

$$\begin{aligned} \texttt {<condition> -> <action> . <continuation process>} \end{aligned}$$

(with a variation for rule (CM1) to be discussed in a minute). For example, lines 3–4 express that the Client process in state 0, in phase NotTaking for its NeedTicket role, as well as in phase NotServed for its NeedService role, can perform the action getTicket and continues as Client(1,c,nt_ph,ns_ph) with control now in state 1, but leaving the parameters c, nt_ph, and ns_ph unchanged. The element-of-list construction nt_ph in [ NotTaking ,Taking ] shows profitable in line 7, for example. Note, the transition is admitted both by phase NotTaking and by phase Taking.

Lines 12–14 embody the contribution of a client process to execution of the $(\text {CM}2)$-rule. If the process resides in trap $\textit{useDone}$ consisting of states 2, 3, and 4 (for all values of variable c), and in phase $\textit{Taking}$ regarding its $\textit{NeedTicket}$ role, then the process is willing to execute the action $\textit{useDone}$ and to continue with its $\textit{NeedTicket}$ phase changed from $\textit{Taking}$ to $\textit{NotTaking}$ as consistency rule $(\text {CM}2)$ prescribes. Note, no for $(\text {CM}2)$ the client process doesn’t depend on other processes.

Consistency rule $(\text {CM}1)$ in which both a client process and the machine process are involved requires their interaction. Assuming Client is in state 1, hence in trap $\textit{requestMachine}$ as the value of c doesn’t matter for this, as well as in phase $\textit{NotTaking}$, then Client is willing to input the value m of the ticket as offered by the machine. But, a priori this value is not known to the client. Therefore, the value is abstracted away by the summation sum m:Nat over all possible values for m. Upon synchronization with the machine process the actual value for m will be handed over. However, this can only happen if the interacting $\textit{Machine}$ process has reached the proper trap in the proper phase regarding the corresponding role.

To enforce synchronization of processes, $\texttt {mCRL2}$ provides the allow-and-communicate mechanism. Once all processes have been specified (Client, Machine, Baker, and Display) the so-called initial process is given. We have chosen to analyze a typical situation of three clients in combination with one machine, one baker, and one display:

The crucial point is, the synchronized execution of the actions requestMachine(n) by Client and readyToProvide(n) by Machine, for the same value n, will be represented by the execution of the action CM1(n) of the overall system. On top of this, for all n, the action CM1 is allowed to be executed, as mentioned in the list of allowed actions, but the action requestMachine and the action readyToProvide on their own are not, since they are deliberately missing from the list of allowed actions. Thus, a requestMachine or readyToProvide cannot happen alone, but combined into the action CM1 only, provided the actions carry the same value for their parameter. Since, by the sum construction the client is willing to perform requestMachine(m) for each value of m, it can match the specific value for m offered by the machine in readyToProvide(m). This way, for this basic case, passing of parameter values from one process to another is achieved.

In general, a Paradigm model $( C_h )_{h \in H}$ will be encoded in mCRL2 as the parallel composition of $\#H$ processes, with $\#H$ the number of elements of the index set H. For a process $C_h$ we have in its encoding, on the one hand, a parameter $\texttt {st}$ of type Nat enumerating the set of states $S_h$ and parameters $\texttt {d}_{1}, \ldots , \texttt {d}_{n_h}$ of properly chosen built-in or user-defined type to represent the extended state of $C_h$, and, on the other hand, parameters $\texttt {ph}_{1}, \ldots , \texttt {ph}_{n_h}$ for each of the roles, each of type specifically introduced for the roles. The actions of the processes are either local actions, from the respective action sets A, together with action corresponding to traps of the various roles of the components. With the combined use of allow and communication operators synchronization of traps can be enforced.

A local transition $\langle s_h, e_h, \psi _h \rangle _{h {\in } H} \xrightarrow {\,a\,} \langle s'_h, e'_h, \psi _h \rangle _{h {\in } H}$, say with $e_h = ( e_{h,j} )_{j{=}1}^{m_h}$, is easy to handle. We only need to verify that the transition $\langle s_{h_0}, e_{h_0} \rangle \xrightarrow {\,a\,} \langle s'_{h_0}, e'_{h_0} \rangle$ for the active component $h_0$ is admitted by the phases in $\psi _{h_0}$ (see Definition 3). That other processes remain unchanged is implied by the interleaving of the processes. Thus, for each transition $\langle s_{h_0}, e_{h_0} \rangle \xrightarrow {\,a\,} \langle s'_{h_0}, e'_{h_0} \rangle$ in $T_h$ we incorporate for mCRL2 process C_h the non-deterministic branch

and add the action a to the set of actions of the allow operator enclosing the parallel composition of components.

A consistency rule $\gamma = ( \, C_r(\varPhi _r) : \varphi _r(e_r) \xrightarrow {\,\theta _r\,} \varphi '_r(e'_r) \, )_{r \in R}$, say with $e_r = ( e_{r,j} )_{j{=}1}^{m_r}$ and $e'_r = ( e'_{r,j} )_{j{=}1}^{m_r}$, is distributed over all components and roles involved. For each index r in R, we include a non-deterministic branch for process $C_r$ and role $\varPhi _r$ in the mCRL2 process C_r.

The summations sum w_1:W_1 to sum w_n:W_n abstract away the n-1 groups of variables of the components other the component $C_r$ itself (although this cannot be read off from the notation above). Thus, of the variable groups w_1 to w_n only w_r is not bound by a summation. The expressions expr_1 to expr_n, built-up from standard constructs and possibly all of the variables in the n groups w_1 to w_n, are the expressions as occurring in the $\#R$ righthand-sides of the consistency rule. For a successful interaction it is required that all parties agree on the values of the parameters and expressions involved. By taking the sum over all possible (potentially infinitely many) values the process C_r leaves it totally to the other components to decide on the values of their variables, if occurring at all. Moreover, if $\#R > 1$ we add the communication theta_1 | ... | theta_#R -> gamma to the communication operator com enclosing the parallel composition of components, but do not include any of the trap actions theta_1,...,theta_#R. In case $\#R=1$, no communication is introduced, but the trap action will be allowed instead.

Some further caution needs to be put in place though, to deal with summations over infinite data types as possibly occurring in the encoding of the consistency rules. In the various analysis steps with the mCRL2 toolset, in particular statespace generation, the tools may hang because of infinite branching. For Paradigm with data, in concrete situations, simplifications to the coding are applied for variables whose actual value is not used. There are two flavors of this: comparison of an expression involving the variable to an expression involving another (as for the ticket number of the client and the baker in lines 21, 24, and 27), or when the variable doesn’t occur at all in the expressions at the righthand-side of the the consistency rule. As illustration of the latter situation, the encoding for the $\textit{Machine}$ process for the consistency rule $(\text {CM}1)$ reads

where no abstraction of the variable c of Client is needed. The machine just provides a ticket number, in our modeling, independent of the actual value of c.

5 Concluding Remarks

We have shown, with the IWIM model in mind, how the coordination modeling language Paradigm can be extended to deal with data. The present set-up is relatively liberal in the use of variables, although in concrete modeling situations a relatively small number of patterns of data flow among interacting components seem to suffice. Further investigation needs to reveal if this allows for a simplification of the consistency rule format and the associated closedness requirements both for sets of consistency rules as well as for the restriction on updates of variables within a trap.

Currently, for formal analysis using the mCRL2 toolset, the encoding needs to be tailored to avoid infinite branching during statespace generation. The toolset provides a number of tools, e.g. lpssumelm and lpsconstelm, that manipulate intermediate artifacts (in so-called linear process specification or lps format) to reduce the specification, leading to smaller and hence more amenable verification problems. It is a topic of further research to develop sum elimination techniques specifically targeting the encoding of consistency rules discussed in this paper.

Application areas for Paradigm with data include the modeling of services, where both coordination and data play a prominent role, as well as the analysis of security protocols. Dissertational work by the second author is underway dealing with the modeling with Paradigm of anonymous networking and internet voting.

Appendices

A Complete mCRL2 Specification of the Bakery Example

This appendix contains the mCRL2 code of the bakery example of Sect. 3.

B Reduced LTS

Labeled transition system for the specification of Appendix A with only actions thankGreet by the Baker process shown on the left. It validates that all three clients are served, assuming an atomic welcome-help-thankGreet sequences of actions, and are served in order of their tickets. On the right, the labeled transition system for the specification of Appendix A with only actions thankLeave by the Client processes shown. It validates that all three clients are served, but they can (and will) leave in any order.

Labeled transition system for the specification of Appendix A with only actions showTicket and clarify by the Client processes shown. It validates that all three clients can raise their ticket independently, since admitted local behavior can be executed asynchronously from other component behavior, but are served in order of their ticket.