Compatibility of software components: modelling and verification

Abstract

The area of Component Based Software Engineering (CBSE) is rapidly emerging as a means of mitigating the complexity faced by software architects during the design and maintenance of large software systems. Unfortunately, given the substantial number of components that may be deployed in a given software architecture, successfully establishing compatible interaction amongst components can be a difficult problem to solve. The purpose of this work is to show that compatibility between components may be determined by developing a formal model to describe component interfaces and their behaviour. In addition to promoting reuse and substitutability in the design and maintenance of software systems, this approach may also have a significant effect on the reliability and trustworthiness of software systems. -- At a fundamental level, a component can be regarded as a cohesive logical unit of abstraction with well-defined interfaces that provide services to its environment or request such services. This work sets the foundation for a formal model of component composition by using Petri nets to represent the behaviour of component interfaces. Compatibility is established by verifying that interfaces can satisfy all requested sequences of operations. The requires and provides relationships are discussed in the context of formal languages generated by the corresponding labelled Petri net models. The compatibility of the interfaces is determined by examining various structural and reachability properties of the net obtained by the composition of the interfaces. -- As commercial components become increasingly available and the web services industry becomes more vibrant, formal compatibility assessment is an important step toward the construction of large, distributed software systems.