Detection and Verification of Semantic Interaction In AOSD

Aspects in Aspect Oriented Software Development (AOSD) may interact with the base system in an unfavorable way, resulting in the degradation of the overall software stability. The interaction caused by the new aspectual introduction alters the base system behavior in an undesired way. Temporal logics, such as Computation Tree Logic (CTL), are used to represent the systempsilas behavior and model checking is used to verify them. Such interaction is referred to as aspect-base interaction. We are proposing a new modular approach to detect such interactions, where aspects are model-checked separately from the base model. This will allow us to detect and report any aspects that violate the base system behavior expressed as CTL. Our modular approach is based on model checking of CTL properties utilizing existing model checkers.