Safety Verification of Software Component Behavior Adaptation

The behavior adaptation of Software component is a crucial problem in component-based software engineering. Software component adaptation aims at generating, as automatically as possible, adaptors to compensate behavior mismatch during components interaction, and ensure the deadlock-freedom of components interaction at the architectural level. A general and safe approach is proposed to solve the behavior mismatch. Firstly, the model of component behavior adaptation and the definition of adaptor are given. Then, the formal specification of component behavior protocol is given and the safety of component behavior adaptation is verified formally. The adaptor can make the correctness of the component interaction with data exchange, and realize the reordering of message. Finally, an example is presented to illustrate the validity of the approach proposed in this paper.