2.7 Example

We will show the implications of our approach by means of a well-known example. Consider the architecture of a typical Producer-Consumer system. This architecture is built from three interconnected components: a Producer, a Consumer, and a temporal store that we can describe as a Buffer. Suppose that the Producer generates several items and sends them to the Buffer, using an operation in, until it decides to quit, which is notified by sending a predefined event wquit. On the other hand, the Consumer retrieves items from the Buffer, using and operation out, and performs some computations with them. The Consumer ends when it has got all the items generated by the Producer, which is notified by the Buffer with an event rquit.

**Figure 1:** Architecture of a Producer-Consumer system
$\begin{figure} \centering \begin{tabular} {\vert p{8.5cm} \vert p{6cm} \vert} \... ...\\ gt\}\end{tabbing}\end{tt}\end{footnotesize}\\ \hline\end{tabular}\end{figure}$

From the description above, we can derive the specification of the interface of the components. Events in and wquit form the interface between the Producer and the Buffer, while out and rquit form the interface between the Buffer and the Consumer. Figure 1 (left) shows what could be the specification of our system in a typical ADL. The Producer-Consumer system is a composite which contains three sub-components, each one instance of a certain component class. These subcomponents (to be more exact the roles that represent their interfaces) are attached to each other, making the previously described interfaces.

The correctness of the attachments can be determined by static analysis, checking the conformance of the names of the operations and the type of the parameters, but mere type checking doesn't ensure that the system will not crash during execution. For instance, the Consumer can invoke an out operation when the Buffer is empty and the Producer has quitted the system. This behavior will lead to a deadlock or a run-time error, depending on the actual implementation of the operations. Thus, a correct performance of the system requires that the components involved follow a certain protocol.

In our example, the Producer may invoke in an undefined number of times, but it must finish sending an wquit event. This behavior must be specified by the role Writer. On the other hand, the Buffer is defined by two roles. Role Input must indicate that the Buffer is able to accept either in or wquit at any time, but always ending in wquit after a sequence of in operations, while role Output must specify that the Buffer will perform out operations only when it is not empty, and that a rquit event will be sent when the Buffer empties after the Producer has quitted. Since the Consumer doesn't know whether these conditions have occurred or not, this will be specified as an nondeterministic behavior of the Buffer, using local choices. Finally, the Consumer must perform out operations until it receives a rquit event, this being described in role Reader as a deterministic behavior, using global choices. Figure 1 (right) shows the specification of system sub-components and their roles.

Role protocols can be specified in the $\pi$ -calculus (but they are not included here to avoid detailed explanations about the syntax and semantics of the calculus), and we could analyze the compatibility of the attachments Input <> Writer and Output <> Reader, finding out that the architecture is composable. Thus, an instance of this architecture, such as

However, not every Producer-Consumer system follows exactly these protocols. Let's consider a certain Producer' which generates exactly four items before quitting. Let role Writer' describe this behavior. Using the relation of role inheritance, we can verify that Writer' inherits from Writer, and thus Producer' inherits from Producer. Hence,

prodcon' : Producer-Consumer(p : Producer');

an instance of Producer-Consumer in which the Producer has been replaced with an instance of Producer', will be also deadlock-free.

Similarly, we could extend our Buffer with an operation flush, that empties the Buffer, and add this new behavior to the Input role. Once again, we can verify that the new Buffer' inherits from Buffer. Thus, Buffer' can be used in any system containing a Buffer, as in

prodcon'' : Producer-Consumer(p: Producer'; b : Buffer');

In conclusion, a single proof of role inheritance allow the replacement of a component in any system belonging to a family of related (but not identical) systems. Liveness properties of the architecture are ensured by static checking even in a scenario of dynamic, i.e. at run-time, binding.