Component Compatibility and Its Verification

An approach to verification of component compatibility is proposed in which each component´s behaviour (at its interfaces) is represented by a labeled Petri net in such a way that the sequences of services (provided or requested) correspond to sequences of labels assigned to occurring transitions. The behaviour of a component can thus be defined as the language of its modeling net. Two interacting components are compatible if and only if all possible sequences of services requested by one of these two components can be satisfied by the other component; in other words, two components are compatible if the language of the requesting component is a subset of the language of the component providing the services. Verification of this simple relation depends upon the class of languages defining the behaviours of the components. If the languages are regular, the verification of compatibility is straightforward. For non-regular languages, a more elaborate approach is needed in which a net model composed of the interacting components is checked for the absence of deadlocks. Some applications of the proposed approach are also discussed.