next up previous
Next: Discussion Up: Avoiding state-explosion by pairwise Previous: Avoiding state-explosion by pairwise

Applying pairwise composition to component assembly

To apply the pairwise method to components, we must be able to define the pairwise interaction amongst components. We do this by extending the component model so that each component is accompanied by several BIA [7,20], one for each of the other components that interacts directly with. The BIA provides information about the externally observable temporal behavior of the component. For example, such an automaton could provide information on the order in which a component makes certain method calls to other components.

Given two components and their BIA, we construct the pair-machine for their interaction by simply taking the automata-theoretic product of the BIA. We can then model check the pair-machine for the desired behavioral compatibility among the two components. If successful, we can then use this pair-machine as input to the pairwise method, as discussed above.



David H. Lorenz 2003-06-30