Siphon-based verification of component compatibility

Zuberek, W.M.

Proc. 4-th Int. Conference on Dependability of Computer Systems (DepCoS-09), Brunow Palace, Poland, June 30 - July 2, 2009, pp.123-132, IEEE CS Press 2009 (ISBN 0-7695-3179-3).


In component-based systems, two interacting components are compatible if any sequence of services requested by one component can be provided by the other. This concept of compatibility can be easily extended to a set of interacting components. Checking the compatibility of interacting components is essential for any dependable software system. Recently, an approach to verification of component compatibility has been proposed in which the behavior of individual components (at component interfaces) was modeled by labeled Petri nets. Moreover, the composition of interacting components was designed in such a way that all component incompatibilities were manisfested by deadlocks in the composed model. Consequently, the verification of component compatibility is performed by deadlock analysis of the composed net model. One of techniques for deadlock analysis is based on net structures called siphons. Siphon-based verification of component compatibility is the subject of this paper.


Petri nets, deadlock detection, structural methods, minimal siphons, basis siphons, linear programming.

Available in pdf.