2.4 Composability

One of the properties that we may analyze in a software architecture is composability , which we could define as the capability of the system of being composed by combining its components as indicated in its architecture. Composability can be checked by determining whether the components of the system are compatible or not. Furthermore, in order to enhance reusability, we should be able to check if a certain existing component can be used in a new system where a similar function is required. Again the intuitive notion of compatibility arises.

Compatibility could be determined by composing in parallel the specifications in $\pi$-calculus of system components. Then, the resulting system would be analyzed for deadlock. However, this would be impractical for complex systems, as it requires the analysis of all the interaction traces of large specifications. Instead of that, we propose the use of explicit interface specifications, or roles , for each connection or attachment between components of the system, indicating the behavior of those components as seen from outside. Then, each attachment between roles is checked locally for compatibility. This reduces the complexity of the analysis to a great extent.

Thus, a software component will be specified by set of roles, which describe its behavior in relation to the other components it is attached to. Each role describe the protocol that the component follows with respect to a certain attachment. Our notion of role derive from the Hiding operator (/L) defined in [Mil89] for CCS, and roles may be considered as partial specifications of the interface of a component. As we usually want to attach roles that match only partially, equivalence checking, using for instance the bisimilarity relations established for the $\pi$-calculus, is not well suited for our purposes. Thus, we have defined a relation of protocol compatibility in the context of $\pi$-calculus. This relation ensures that two components, represented by a pair of roles, will be able to interact without deadlock until they reach a well-defined final state. In this context, the analysis of the composability of a software architecture is reduced to local analysis of compatibility. Compatibility ensures that any software system built according to the specifications of the architecture will not produce a deadlock caused by the interaction in any attachment between its components.

A formal proof of the properties of compatibility is out of the scope of this paper, but it can be found in [CPT97]. Compatibility analysis can be easily automated in a similar way to the characterization devised by Sangiorgi for the bisimilarity relations [San93].