Petri Nets in modeling component behavior and verifying component compatibility

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

Proc. Int. Workshop on Petri Nets and Software Engineering (PNSE'07), part of the 28-th Int. Conf. on Application and Theory of Petri Nets and Other Models of Councurrency, Siedlce, Poland, 25-26 June 2007, pp.160-174.


In component-based systems, two components are compatible if all possible sequences of services requested by one component can be provided by the other component. Verification of component compatibility is essential in large software systems as otherwise subtle software failures can exist which are difficult to detect through software testing. 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, and such component models are composed. The composition operation is designed in such a way that component incompatibilities are manifested as deadlocks in the composed model. Compatibility verification is thus performed through deadlock detection in the composed models. Efficient structural techniques are proposed for deadlock analysis.


Software components, component-based systems, component compatibility, compatilibility verification, Petri nets, deadlock detection, structural analysis.


Available in pdf.