Model fusion for the compatibility verification of software components

Zuberek, W.M.

in Proc. of the Ninth IEEE Int. Conf. on Dependability of Computer Systems (DEPCOS-14), Brunow Palace, Poland, June 30 - July 4, 2014, Springer Int. Publ. Switzerland 2014, pp.521-529.


Similarly as in earlier work on component compatibility, the behavior of components is specified by component interface languages, defined by labeled Petri nets. In the case of composition of concurrent components, the requests from different components can be interleaved, and - as shown earlier - such interleaving can result in deadlocks in the composed system even if each pair of interacting components is deadlock--free. Therefore the elements of a component--based system are considered compatible only if the composition is deadlock--free. This paper formally defines model fusion, which is a composition of net models of individual components that represents the interleaving of interface languages of interacting components. It also shows that the verification of component compatibility can avoid the exhaustive analysis of the composed state space.


software components, component-based systems, component composition, component compatibility, compatibility verification, model fusion, labelled Petri nets


Available in pdf.