Alloy-Based Lightweight Verification for Aspect-Oriented Architecture

ccJava, a new kind of class-based AOP language, provides the weaving-interface mechanism in which the weaving can be realized by the component-and-connector architecture. The interface description constructs in ccJava can be considered a kind of architecture description language that takes into account the weaving. This paper provides a lightweight verification approach using Alloy, a structural modeling language based on relational logic. Using Alloy, we can verify whether the weaving based on the component-and-connector architecture satisfies some kinds of properties--whether advice-types are specified correctly,whether a pointcut selects join points correctly, and so on. By enforcing the architecture verified by Alloy to the class implementation, we can construct a reliable system.