Formalization of Component Substitutability

Component-Based Software Engineering (CBSE) is increasingly used to develop large scale software. In this context, a complex software is composed of many software components which are developed independently and which are considered as black boxes. Furthermore, they are assembled and often dependent from each other. In this setting, component upgrading is a key issue, since it enables software components to evolve. To support component upgrading, we have to deal with component dependencies which need to be expressed precisely. In this paper, we consider that component upgrade requires managing substitutability between the new and the old components. The substitutability check is based on dependency and context descriptions. It involves maintaining the availability of previously used services, while making sure that the effect of the new provided services do not disrupt the system and the context invariants are still preserved. We present here a formal definition and a verification algorithm for safe component substitutability.