Verification of Component Behavioral Compatibility

D.C. Craig, and Zuberek, W.M.

Proc. 2-nd Int. Conf. on Dependability of Computer Systems (DepCoS-07), Szklarska Poreba, Poland, 14-16 June 2007, pp.294-304.


In component-based systems, two components are behaviorally compatible if all possible sequences of services requested by one component can be provided by the other component. Verification of this compatibility is essential if subtle software failures, which are difficult to detect and correct, are to be eliminated. For verification of compatibility, the behavior of interacting components, at their interfaces, is modeled by labeled Petri nets with labels representing the requested and provided services. The paper discusses the verification process for several classes of interface languages, with emphasis on the algorithmic aspects of verification.


Software architecture, software components, component compatibility, Petri nets, deadlock detection.


Available in pdf.