A type language for message passing component-based systems

Code reusability is an important principle to support the development of software systems in a cost-effective way. It is a key principle in Component-Based Development (CBD) [16], where the idea is to build systems relying on the composition of loosely-coupled and independent units called components.

The motivations behind CBD are, on the one hand, to increase development efficiency and lower the costs (by building a system from pre-existing components, instead of building from scratch), and on the other hand, to improve quality of the software for instance to what concerns software errors (components can be tested over and over again in different contexts). Consider, for example, microservices (see, e.g., [9]) that have been recently adopted by massively deployed applications such as Netflix, eBay, Amazon and Uber, and that are reusable distributed software units. In such a distributed setting, composing software elements necessarily involves some form of communication scheme, for instance based on message passing.

In order for the functionality to be achieved, communication among components should follow a well-defined protocol of interaction, that may be specified in terms of some choreography language like, for example, WS-CDL [19] or the choreography diagrams of BPMN [18]. A component should be able to carry out a certain sequence of I/O actions in order to fulfil its role in the protocol. One way to accomplish this is to implement a component in a way that prescribes a strict sequence of I/O actions, that should precisely match the actions expected by the protocol. However, this choice interferes with reusability, since such a component can be used only in an environment that expects that exact sequence of communication actions. For instance, if a component receives an image and outputs its classification just once, what will happen if we need to use this component in a context that requires the classification is sent multiple times?

In contrast, a more flexible design choice inspired by reactive programming is to design components so that they can respond to external stimulus without any specific I/O sequence. The reactive programming principle for building such components is to consider that as soon as the data is available, it can be received or emitted. For example, we can design a component that is able to output a classification after receiving an image, as long as required. In such a way, reusability is promoted since such components can be used in different environments thanks to the flexibility given by the reactive behaviour. However, such a flexibility at the composition level may be too wild if all components are able to send / receive data as soon as it is available. Hence, there is the need to discipline the interactions at the level of the environment where the composition takes place. What if, for example, we have different images that need to be classified and the classifying component is continuously emitting the result for the first image?

Carbone, Montesi and Vieira [6] proposed a language that supports the development of distributed systems by combining the notions of reactive components with choreographic specifications of communication protocols [17]. The proposal considers components that can dynamically send / receive data as soon as it is available, while considering that an assembly of components is governed by a protocol. Hence, among all the possible reactions that are supported by the composed components, the only ones that will actually be carried out are the ones allowed by the protocol. A composition of components defines itself a component that can be further composed (under the governance of some protocol) also providing a reactive behaviour. This approach promotes reusability thanks to the flexibility of the reactive behaviour. For instance, by abstracting from the number of supported reactions, e.g., if a component can (always) perform a computation reacting to some data inputs, then it can be used in different protocols that require such computation to be carried out a different number of times; by abstracting from message ordering, e.g., if a component needs some values to perform a computation, it may be used with any protocol that provides them in any order.

Component implementations should be hidden, so it shouldn’t be necessary to inspect the inner workings in order to asses if it is usable in a determined context for the purpose of off-the-shelf substitution or reuse. Hence, a component should be characterised with a signature that allows checking its compatibility when used in a composition. In particular, it must be ensured that each component provides (at least) the behaviour prescribed by the protocol in which the component participates. Carbone et al. [6] propose a verification technique that ensures communication safety and progress. However, the approach requires checking the implementation of components each time the component is put in a different context, i.e., each time that the component is used “off-the-shelf” we need to check if the reactions supported by the component are enough to implement its part in the protocol.

In this work we consider a different approach, avoiding the implementation check each time a component is to be used. Firstly, we introduce a type language that characterises the reactive behaviour of components. Secondly, we devise an inference technique that identifies the types of components, based on which we can verify whether the component provides the reactive behaviour required by a context. The motivation is in tune with reusability: once the component’s type is identified, there is no further need to check the implementation, because the type is enough to describe “what the component can do”.

Our types specify the ability of components to receive values of a prescribed basic type. Moreover, they track different kinds of dependencies, for instance that certain values to be emitted always (for each output) require a specific set of inputs (dubbed per each value dependencies). Our types can also describe the fact that a component needs to be, in some sense, initialised by receiving specific values before proceeding with other reactive behaviour (dubbed initial dependencies). Furthermore, our types also identify constraints on the number of values that a component can send. Finally, we ensure the correctness of our type system by proving that our extraction procedures are sound with respect to the semantics of the Governed Components (GC) language [6], considering here the choice-free subset of the GC language and leaving a full account of the language to future work. Moreover, we ensure that whenever a type of a component prescribes an action, a component will not be stuck, i.e., it will eventually carry out the matching action.

The rest of the paper is organised as follows. We first present the GC language in Section 2. Then in Section 3 we intuitively introduce our type language through a motivating example based on AWS Lambda [2] where we point out different scenarios that might occur while composing components and how our types allow to describe certain behavioural patterns. Section 4 introduces the syntax and the semantics of our types. Then, we define the type extraction for base components in Section 4.1, whereas the type extraction for composite components in Section 4.2. In Section 4.3 we present our results. Section 5 concludes, discusses related work and gives some future issues.

In this section we briefly introduce the GC language, focusing on the main points that allow to grasp the essence of the model and to support a self-contained understanding of this paper. We refer the interested reader to [6] for a full account of the language. The syntax of the (protocol choice-free fragment of the) GC language is given in Table 1. There are two kinds of components ($K$): base and composite. Both kinds interact with the external environment by means of input and output ports exposed as the component’s interface. Besides of the interface, components are defined by their implementation.

In the case of a base component the implementation is given by the list of local binders ($\{L\}$). A local binder specifies a function, denoted as $y=f(\tilde{x})$, which is used to compute the output values for port $y$ relying on values received on list of (input) ports $\tilde{x}$. So, we say that component’s ability to output a value may depend on the ones received, where instead, components are always able to receive values.We abstract from the definition of such functions $f$ and assume them to be total. Received values are processed in a FIFO discipline, so queues are added to the local binders at runtime (noted as ${y}\,=\,{f(\tilde{x})}\,\langle\,{\tilde{\sigma}}$). Each element ($\sigma$) in a queue ($\tilde{\sigma}$) is a store defined as a partial mapping from input ports to values ($\tilde{\sigma}=\sigma_{\_}1,\sigma_{\_}2,\ldots,\sigma_{\_}k$, where in $\sigma_{\_}1$ the oldest values received are stored, in $\sigma_{\_}2$ the second-oldest values, and so on and so forth up to $\sigma_{\_}k$). E.g., if $y=f(x_{\_}1,x_{\_}2)<\cdot$ and the component receives $v_{\_}1$ and $v_{\_}2$ in that order on port $x_{\_}1$ and $v_{\_}3$, $v_{\_}4$ and $5$ on port $x_{\_}2$. The queue at this point has three mappings $(x_{\_}1\rightarrow v_{\_}1,x_{\_}2\rightarrow v_{\_}3),(x_{\_}1\rightarrow v_{\_}2,x_{\_}2\rightarrow v_{\_}4),(x_{\_}2\rightarrow 5)$ where two are “complete” to compute the function and one is not.

The implementation of a composite component, represented by $\{G;R;D;\mathsf{r}[F]\}$, is an assembly of subcomponents whose interaction is governed by a protocol ($G$). The set of subcomponents are given in $R$ together with their roles in the interaction (e.g., $\mathsf{r}=K$ denotes that component $K$ is assigned to role $\mathsf{r}$). Composite components also specify a list of (distribution) binders ($D$) that provide an association between the messages exchanged in the protocol ($\ell$) and the ports ($x,y$) of the components (e.g., $\mathsf{p}.{x}\mathrel{\stackrel{{\scriptstyle{\;\;\ell\;\;}}}{{\mbox{\leftarrowfill}}}}{\mathsf{q}.{y}}$ states that a message with a label $\ell$ is emitted on port $y$ of the component assigned to role $\mathsf{q}$, and to be received on port $x$ of the component assigned to role $\mathsf{p}$). Ports are uniquely associated to message labels ($\ell$) in such way that each communication step in the protocol has a precise mapping to a port, i.e., all values emitted on a port will be carried in messages with the same label and all values received on a port will be delivered in messages with the same label. E.g., every time a value is emitted from some port $y$ it will be carried in a message labelled with e.g., $\ell$ and a value delivered on some port $x$ is delivered on a message with the same label $\ell$. Some other label cannot be attached to $y$, otherwise the association would not be unique. The $class$ message label (or some other) cannot be attached to $y_{\_}p$ otherwise the association would not be unique. Finally, subterm $\mathsf{r}[F]$ is used to specify the externally-observable behaviour: the (only interfacing) subcomponent responsible for the interaction with the external environment is identified (by its role $\mathsf{r}$) and the respective connection between ports is provided by forwarders ($F$). The idea is that values received on the (input) ports of the composite component are directly forwarded to the (input) ports of the interfacing subcomponent, and values emitted on the (output) ports of the interfacing subcomponent are forwarded to the (output) ports of the composite component. For example, the term $x^{\prime}\leftarrow x$ is for forwarding an input, and the term $y\leftarrow y^{\prime}$ is for forwarding an output ($x$ and $y$ are the ports of the composite component).

Protocol specifications prescribe the interaction among a set of parties identified by roles. Communication term $\mathsf{p}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;\ell\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{\tilde{q}};G$ specifies that role $\mathsf{p}$ sends the message labelled $\ell$ to the (nonempty) set of roles $\tilde{\mathsf{q}}$, after which the protocol continues as specified by $G$. The difference between this work and [6] is the absence of branching. Then we have terms $\mu\mathbf{X}.G$ and $\mathbf{X}$ for specifying recursive protocols. Finally, term $\mathbf{end}$ defines the termination of the protocol.

We now present the operational semantics of the GC in terms of a labelled transition system (LTS). We denote by $K\ \mathrel{\stackrel{{\scriptstyle{\;\;\lambda\;\;}}}{{\mbox{\rightarrowfill}}}}\ K^{\prime}$ that a component $K$ evolves in one computational step to $K^{\prime}$, where observations are captured by labels defined as follows $\lambda::=x?v\ |\ y!v\ |\ \tau$. Transition label $x?v$ represents an input on port $x$ of a value $v$, label $y!v$ captures an output on port $y$ of a value $v$, and label $\tau$ denotes an internal move.

The rules that describe the behaviour of components are presented in two parts, addressing base and composite components separately. We present only the main rules, the full semantics can be found in [6].

Rules $\mathsf{OutBase}$ and $\mathsf{InpBase}$ that are given in Table 2 capture base component behaviour, and are defined relying on transitions exhibited by local binders, denoted $L\ \mathrel{\stackrel{{\scriptstyle{\;\;\lambda\;\;}}}{{\mbox{\rightarrowfill}}}}\ L^{\prime}$. Rule $\mathsf{OutBase}$ states that if local binders $L$ can exhibit an output of value $v$ on port $y$, where $y$ is part of the component’s interface, then the corresponding output can be exhibited by the base component. Rule $\mathsf{InpBase}$ follows the same lines.

Notice that the transition of the local binder specifies a final configuration $L^{\prime}$ which is accounted for in the evolution of the base component. We omit here the rules for local binders (see [6]) and provide only an informal account for them. Essentially, a (runtime) local binder ${y}\,=\,{f(\tilde{x})}\,\langle\,{\tilde{\sigma}}$ is always receptive to an input $x?v$: if $x$ is not used in the function ($x\not\in\tilde{x}$) then value $v$ is simply discarded; otherwise, the value is added to the (oldest) entry in mapping queue $\tilde{\sigma}$ that does not have an entry for $x$ (possibly originating a new mapping at the tail of $\tilde{\sigma}$). All local binders in $L$ synchronise on an input, so each local binder will store (or discard) its own copy of the value. Instead, local binder outputs are not synchronised among them: if a local binder outputs a value, other local binders will not react. For this to happen, the oldest mapping in queue $\tilde{\sigma}$ must be complete (i.e., assign values to all of $\tilde{x}$) at which point function $f$ may be computed, the result which is then carried in the transition label (i.e., the $v$ in $y!v$).

We now introduce the rules that capture the behaviour of the composite components, displayed in Table 3. Notice that a composite component may itself be used as a subcomponent of another composition (of a “bigger” component), and base components provide the syntactic leaves. Rules $\mathsf{OutComp}$ and $\mathsf{InpComp}$ capture the interaction of a composite component with an external environment, realised by the interfacing subcomponent. The role assignment $\mathsf{r}\!=\!K$ captures the relation between component $K$ and role $r$, which is specified as the interfacing role ($\mathsf{r}[F]$). Rule $\mathsf{OutComp}$ allows for the interfacing component $K$ to send a value $v$ to the external environment via one of the ports of the composite component ($y$). Notice that the connection between the port of the interfacing component ($z$) and the port of the composite component ($y$) is specified in a forwarder ($F=y\leftarrow z,F^{\prime}$). Rule $\mathsf{InpComp}$ follows the same lines to model an externally-observable input. Rule $\mathsf{Internal}$ allows for internal actions in a subcomponent ($K$), where the final configuration ($K^{\prime}$) is registered in the final configuration of the composite component.

Rules $\mathsf{OutChor}$ and $\mathsf{InpChor}$ capture the interaction among subcomponents of a composite component. Rule $\mathsf{OutChor}$ addresses the case when a component is sending a message to another one. The premises, together with role assignment $\mathsf{p}\!=\!K$, establish the connection among sender component $K$, the component port $u$, sender role $\mathsf{p}$, and message label $\ell$. Premise $K\ \mathrel{\stackrel{{\scriptstyle{\;\;{u}!{v}{}\;\;}}}{{\mbox{\rightarrowfill}}}}\ K^{\prime}$ says that the sender component ($K$) can perform an output of value $v$ on port $u$. Premise $D=\mathsf{q}.{z}\mathrel{\stackrel{{\scriptstyle{\;\;\ell\;\;}}}{{\mbox{\leftarrowfill}}}}{\mathsf{p}.{u}},D^{\prime}$ says that the distribution binders specify the (unique) relation between port $u$ of sender role $\mathsf{p}$ and message label $\ell$ (receiver role $\mathsf{q}$ and associated port $z$ are not important here). The last premise $G\ \mathrel{\stackrel{{\scriptstyle{\;\;\mathsf{p}!\ell\langle v\rangle\;\;}}}{{\mbox{\rightarrowfill}}}}\ G^{\prime}$ realises the component governing the protocol, i.e., saying that the communication is only possible if the protocol prescribes it. Namely, the premise says that the protocol exhibits an output of a value $v$ carried in message $\ell$ from role $\mathsf{p}$. The rules for protocol transitions are presented in [6]. Naturally which semantics has an impact on our technical development (namely regarding end-point projection in local protocols), but to some extent can be addressed in a modular way (i.e., up to the existence of the end-point projection). Notice that the transitions of component $K$ and protocol $G$ specify final configurations $K^{\prime}$ and $G^{\prime}$ which are accounted for in the evolution of the composite component.

Rule $\mathsf{InpChor}$ is similar, but instead of message sending, it addresses the case when a subcomponent receives a message from another subcomponent. The premises are equivalent to the ones for Rule $\mathsf{OutChor}$, but now regard reception. Namely, by saying that receiving component $K$ can exhibit the respective input transition, that the distribution binder specifies the relation of message label $\ell$ with receiver role $\mathsf{q}$ and port $z$, and that protocol $G$ prescribes the input of a value.

In order to further motivate GC and also to introduce our typing approach, we now informally discuss an example inspired by a microservices scenario [2] that addresses an Image Recognition System ($\mathsf{IRS}$). The basic idea is that users upload images and receive back the resulting classification. Moreover, users can get the current running version of the system whenever desired. The $\mathsf{IRS}$ is made of two microservices, $\mathsf{Portal}$ and $\mathsf{Recognition}$ $\mathsf{Engine}$ ($\mathsf{RE}$), that interact according to a predefined protocol.

The task is achieved according to the following workflow: $\mathsf{Portal}$ sends the $\mathit{image}$ loaded by a user to $\mathsf{RE}$ to be processed. When $\mathsf{RE}$ service finishes its $\mathit{classification}$, it sends the $\mathit{class}$ as the result of the $\mathit{classification}$ to $\mathsf{Portal}$. We model the scenario in the GC calculus by assigning to each microservice the corresponding role and using components to represent them. We assign role $\mathsf{Portal}$ to component $K_{\_}{Portal}$ and role $\mathsf{RE}$ to component $K_{\_}{RE}$, where $K_{\_}{Portal}$ and $K_{\_}{RE}$ are base components. Interaction between these two components is governed by global protocol $G$, that can be described as: $\mathsf{Portal}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;image\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{RE};\mathsf{RE}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;class\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{Portal}$. This (the part of $G$) protocol exactly specifies the workflow described above: $\mathsf{Portal}$ sends an $image$ to $\mathsf{RE}$ ($\mathsf{Portal}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;image\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{RE}$) that answers with the computed $class$ ($\mathsf{RE}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;class\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{Portal}$). If we add the termination ($\mathbf{end}$) we obtain (complete $G$) protocol $\mathsf{Portal}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;image\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{RE};\mathsf{RE}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;class\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{Portal};\mathbf{end}$, which may be described as a one-shot protocol, since the interaction is over ($\mathbf{end}$) after the components exchange the two messages.

We obtain composite component $K_{\_}{IRS}$ by assembling $K_{\_}{Portal}$ and $K_{\_}{RE}$ together with protocol $G$ that governs the interaction. Below, we show how it is possible to graphically represent component $K_{\_}{IRS}$, where we represent $K_{\_}{Portal}$ and $K_{\_}{RE}$ as its subcomponents:

The subcomponent $K_{\_}{Portal}$ is the interfacing component (hence is the only one connected to the external environment via forwarders). We can specify $K_{\_}{Portal}$ in the GC language as

$$[{x_{\_}p,x_{\_}p^{\prime}}\,\rangle\,{y_{\_}p,y_{\_}p^{\prime},y_{\_}p^{\prime\prime}}]\{y_{\_}p=f_{\_}u(x_{\_}p)<\tilde{\sigma}^{y_{\_}p},y_{\_}p^{\prime}=f_{\_}r(x_{\_}p^{\prime})<\tilde{\sigma}^{y_{\_}p^{\prime}},y_{\_}p^{\prime\prime}=f()<\cdot\}$$

As previewed in the graphical illustration, from the specification we can see that $K_{\_}{Portal}$ component has two input ports ($x_{\_}p,x_{\_}p^{\prime}$), three output ports ($y_{\_}p,y_{\_}p^{\prime},y_{\_}p^{\prime\prime}$), and three local binders that at runtime are equipped with queues ($\tilde{\sigma}^{y_{\_}p}$, $\tilde{\sigma}^{y_{\_}p^{\prime}}$ and empty queue $\cdot$ given that the respective binder does not use any input ports). Notice that the queues are only required at runtime and are initially empty.

The idea of our type description is to provide an abstract characterisation of component’s behaviour. Types provide information about the set of input ports, namely the types of values that can be received on them, and about the output ports, namely regarding their behavioural capabilities. In particular, for each output port there are constraints which comprise three pieces of information: what type of values are emitted; what is the maximum number of values that can be emitted; and what are the dependencies on input ports, possibly including the number of currently available values that satisfy the dependency at runtime.

Informally, the type of $K_{\_}{Portal}$ announces the following: In the two input ports $x_{\_}p$ and $x_{\_}p^{\prime}$ the component can receive an $\mathit{image}$ and a $\mathit{class}$, respectively ({$x_{\_}p(\mathit{image}),x_{\_}p^{\prime}(\mathit{class})\}$). Also, the type says in $y_{\_}p$ the component can emit $\mathit{image}$s and it can do so an unbounded number of times (denoted by $\infty$) as the underlying local binder imposes no boundary constraints. In particular, the local binder can send an $\mathit{image}$ as soon as one is received in $x_{\_}p$. Hence, we have a per each value dependency of $y_{\_}p$ on $x_{\_}p$. Formally, we write this constraint as $y_{\_}p(image):\infty:[\{x_{\_}p\!:\!N_{\_}p\}]$, where $N_{\_}p$ is the number of values received on $x_{\_}p$ that are available to be used to produce the output on $y_{\_}p$. We may describe constraint $y_{\_}p^{\prime}(\mathit{class}):\infty:[\{x_{\_}p^{\prime}\!:\!N_{\_}p^{\prime}\}]$ in a similar way. In constraint $y_{\_}p^{\prime\prime}(\mathit{version}):\infty:[\emptyset]$ there are no dependencies from input ports specified, hence the reading is only that a $\mathit{version}$ can be emitted an unbounded number of times. We may specify the type of $K_{\_}{Portal}$ as:

$$T_{\_}{\mathit{Portal}}=<\{x_{\_}p(image),x_{\_}p^{\prime}(class)\};\{y_{\_}p(image):\infty:[\{x_{\_}p\!:\!N_{\_}p\}],y_{\_}p^{\prime}(class):\infty:[\{x_{\_}p^{\prime}\!:\!N_{\_}p^{\prime}\}],y_{\_}p^{\prime\prime}(version):\infty:[\emptyset]\}>$$

Composite component $K_{\_}{IRS}$ is an assembly of two base components $K_{\_}{\mathit{Portal}}$ and $K_{\_}{RE}$ whose communication is governed by global protocol $G$. The description of $K_{\_}{IRS}$ in GC language is the following:

$$K_{\_}{IRS}=[{x}\,\rangle\,{y,y^{\prime}}]\{G;\mathsf{Portal}=K_{\_}{Portal},\mathsf{RE}=K_{\_}{RE};D;\mathsf{Portal}[F]\}$$

where $G$ is the already described one-shot protocol

$$G=\mathsf{Portal}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;image\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{RE};\mathsf{RE}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;class\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{Portal};\mathbf{end}$$

Interfacing component $K_{\_}{\mathit{Portal}}$ forwards the values from/to the external environment as specified in the forwarders ($F=x_{\_}p\leftarrow x,y\leftarrow y_{\_}p^{\prime},y^{\prime}\leftarrow y^{\prime\prime}_{\_}p$). The forwarding implies that the characterisation of ports $x$, $y$ and $y^{\prime}$ in the type of $K_{\_}{IRS}$ relies on one of the ports $x_{\_}p$, $y_{\_}p^{\prime}$ and $y_{\_}p^{\prime\prime}$, respectively, in the type of $K_{\_}{\mathit{Portal}}$.

The type of $K_{\_}{IRS}$ then says that it can always input on $x$ values of type $\mathit{image}$ accordingly to the input receptiveness principle. The constraint for $y^{\prime}$ is the same as for $y_{\_}p^{\prime\prime}$ since $y_{\_}p^{\prime\prime}$ does not depend on the protocol (in fact it has no dependencies). However, this is not the case for $y$: in order for a $\mathit{class}$ of an image to be forwarded from $y_{\_}p^{\prime}$ there is a dependency (identified in $T_{\_}{\mathit{Portal}}$) on port $x_{\_}p^{\prime}$. Furthermore, component $K_{\_}{\mathit{Portal}}$ will only receive a value on $x_{\_}p^{\prime}$ accordingly to the protocol specification, in particular upon the second message exchange. Hence, there is also a protocol dependency since the first message exchange has to happen first, so there is a transitive dependency to an $\mathit{image}$ being sent in the first message exchange, emitted from port $y_{\_}p$ of component $K_{\_}{\mathit{Portal}}$. Finally, notice that $y_{\_}p$ depends on $x_{\_}p$ which is linked by forwarding to port $x$ of component $K_{\_}{IRS}$, thus we have a sequence of dependencies that link $y$ to $x$.

Since we have a one-shot protocol, the communications happens only once, which implies that one $\mathit{class}$ is produced for the first $\mathit{image}$ received. We therefore consider that the dependency of $y$ on $x$ is initial (since one value suffices to break the one-shot dependency), and that the maximum number of values that can be emitted on $y$ is 1. This constraint is formally written as $y(class):1:[\{x:\Omega\}]$. The constraint for $y^{\prime}$ is $y^{\prime}(version):\infty:[\emptyset]$, where the set of dependencies is empty, i.e., it does not depend on any input. We then have the following type for component $K_{\_}{IRS}$:

$$T_{\_}{IRS}=<\{x(image)\};\{y(class):1:[\{x:\Omega\}],y^{\prime}(version):\infty:[\emptyset]\}>$$

Let us now assume a recursive version of protocol

$$G^{\prime}=\mu\mathbf{X}.\mathsf{Portal}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;image\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{RE};\mathsf{RE}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;class\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{Portal};\mathbf{X}$$

is used instead (i.e., $K_{\_}{IRS}^{\prime}=[{x}\,\rangle\,{y,y^{\prime}}]\{G^{\prime};\mathsf{Portal}=K_{\_}{Portal},\mathsf{RE}=K_{\_}{RE};D;\mathsf{Portal}[F]\}$). The idea now is that for each $\mathit{image}$ received a $\mathit{class}$ is produced. So, $\mathit{class}$ may be emitted on $y$ an unbounded number of times and the dependency of $y$ on $x$ is of a per each kind. Notice that the chain of dependencies can be described as before, but the one-shot dependency from before is now renewed at each protocol iteration.

The constraint for $y$ in this settings is $y(class):\infty:[\{x\!:\!N_{\_}i\}]$, where $N_{\_}i$ captures the number of values received on $x$ that are currently available to produce the outputs on $y$. The constraint for $y^{\prime}$ is the same as in the previous case. We then have that the type of $K_{\_}{IRS}^{\prime}$ is

$$<\{x(image)\};\{y(class):\infty:[\{x\!:\!N_{\_}i\}],y^{\prime}(version):\infty:[\emptyset]\}>$$

Imagine that $K^{\prime}_{\_}{Portal}$ is now a composite component that has an initialisation phase such that, first it receives a message about what kind of classification is required (e.g., “classify the image by the number of faces found on it”), then it sends it to $K^{\prime}_{\_}{RE}$, after which the uploading and classification of the images can start (all other characteristics remain). Let $x_{\_}1$ be the port of $K^{\prime}_{\_}{IRS}$ on which this message is received. Let us consider the following protocol

$$G^{\prime\prime}=\mathsf{Portal}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;kind\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{RE};\mu\mathbf{X}.\mathsf{Portal}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;image\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{RE};\mathsf{RE}\!\!\!\ \mathrel{\stackrel{{\scriptstyle{\;\;class\;\;}}}{{\mbox{\rightarrowfill}}}}\ \!\!\!\mathsf{Portal};\mathbf{X}$$

where after component $K^{\prime}_{\_}{Portal}$ sends the required kind of classifications (labelled as $\mathit{kind}$), the communication between $K^{\prime}_{\_}{Portal}$ and $K^{\prime}_{\_}{RE}$ is governed by a recursive protocol as described in the previous example. The type of the component $K^{\prime}_{\_}{IRS}$ is similar to the type from the previous example, but now announces that the output on $y$ requires an initial value to be received on port $x_{\_}1$, as the image classification process can only start after that. We then have the type of $K^{\prime}_{\_}{IRS}$

$$<\{x(image)\};\{y(class):\infty:[\{x\!:\!N_{\_}i,x_{\_}1:\Omega\}],y^{\prime}(version):\infty:[\emptyset]\}>$$

In this section we define the type language that captures the behaviour of components in an abstract way, starting with the presentation of the syntax which is followed by the operational semantics. Then we present two procedures that define how to extract the type of a component. The first procedure is for base, and the second one is for composite components.