A Model-Based Method for Modeling and Verifying Event-Based Aspect-Oriented Applications

摘要

Event-based aspect-oriented programming (EAOP) model allows to systematically treat relationship between point-cuts and to execute aspects whenever receiving events emitted by the base program. However, this model neither comes with formal specification nor provides any mechanism to verify its properties formally. In this paper, we propose a model-based method based on Event-B formal method to analyze an EAOP application. First, we specify its components in Event-B notations where we make use of Event-B refinement mechanism to model the base and the monitoring programs. After that, we exploit Event-B generated proof obligations to check if the application constraints are affected by aspect cross-cuts. Finally, the proposed method is illustrated in detail with an example.