2 Position

Industry, and especially high technology industry, relies on a set of developed products to accomplish a given task. It is common practice to reuse already developed components, whether ``home made'' or off the shelves. Those components have to be composed, in some way, and there are many of them, to become the system's model.

The need to know, before completion (and even more before begining the developpement itself), that a product will match the clients requirements is of paramount importance. It is thus crucial to know in advance (before begining the development phase) that a system can be constructed that will respect certain properties, knowing the components and their properties it will include.

The standard (mathematical) approach to verification requires a model of the system being verified, a specification method for expressing desired properties and a proof method to show that a model satisfies those properties.

The problem of composition is the problem of the non closure of properties. For instance consider the nonzenoness property (every finte run can be extended to an infinite one) : let P be a component emitting a message at time 0, and upon receiving a message at time $\delta_i$, emits at time $\delta_i + 1/2^i$ for i > 0. Now let Q be another component waiting for an input and once the input arrives at time $\sigma_i$, it emits a message at time $\sigma_i + 1/2^i$, for i > 0. Each component is nonzeno, but their parallel composition is not (time cannot progress past 2).

Figure 1 illustrates that point : what are the "good" abstraction functions and composition operators such that the diagram commutes and such that there exists a way to conclude about the validity of a property on C from those known about ${\cal M}_A$ and ${\cal M}_B$ ?

  

Figure 1: The composition problem