Handling consistency of software evolution in an efficient way

Software evolution by T. Katayama (2001) is about changes to software. A typical evolution scenario is to incorporate additional features into a system. In such a situation, there is a fundamental issue to be dealt with. It is to verify that the extra features do not violate existing properties adhered to the system, i.e. consistency. The verification method is also required to be efficient. This work focuses on the formal solution of these two issues. Systems are essentially structured in terms of features. Between features are interfaces through which features communicate with each other. The consistency between the system (base) and an extra feature (extension) during evolution is then verified via a modular model checking method by K. Fisler and S Krishnamurthi (2001). Instead of checking entirely the newly evolved system, the proposed method only executes in the extension with some base behavior assumption at the interface. This approach turns out to be very efficient as the verification complexity only depends on the extension. Further, the method is very flexible since the interface is open for unanticipated software changes. A case study is also provided to illustrate two eminent merits of the approach - efficiency in consistency verification and openness.