Modeling and verification of compatibility of component composition

D. Craig and Zuberek, W.M.

Proc. 3-rd Workshop on Modeling of Objects, Components, and Agents (MOCA'04), Aarhus, Denmark, 11-13 October 2004, pp.117-130.


Two components are compatible if any sequence of operations requested by one of these components can be provided by the other component. If the set of all requested sequences is denoted by LR and the set of all provided sequences of operation by LP, then the two components are compatible if LR is a subset of LP. This paper uses Petri nets to model the interface behaviors of interacting components and formally defines the composition of components. Compatibility of components is verified by checking if the composed models contain deadlocks. Simple examples illustrate the proposed approach.


Component compatibility, component interfaces, software architecture, component-based software, Petri nets, deadlock detection.


Available in pdf.