Model checking for aspect-oriented software evolution
Wuttipong Ruanthong, Pornsiri Muenchaisri · International Conference on Software Engineering · 2005
Model checking is the verification approach for proving a satisfaction of desired properties on a finite state system model. Whenever a new feature (aspect) which is developed as a separated unit is composed to the original software for evolving to the next generation, the properties which held on the model of the original software should be re-checked for their preservation. The re-verification of those properties with the traditional method is impractical because the state space of that software model is increased after the evolution. We use model checking for verifying the evolving software model based on the aspect-oriented concepts. The proposed for the preservation checking called certainty -aware technique can reduce time and state space in the process of preservation checking. Therefore, the verification process of model checker which utilizes our can be completed faster than the verification process of traditional model checker.