Model Fusion for the Compatibility Verification of Software Components

Abstract

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.