A formal approach facilitating the evolution of component-based software

The component-based approach is very effective in software development and evolution. The most challenging issue of the approach is component composition. Though components are syntactically compatible in their interfaces, once plugged together, they do not perform as expected because components are semantically inconsistent with each other, i.e. the component consistency problem. This paper gives a formal approach to strengthen component specification by including component semantic written in the temporal logic CTL. Based on this semantic information, components can be efficiently cross-checked for their consistency, even for future unanticipated component extensions during system evolution.