2008 Sixth International Conference on Software Engineering Research, Management and Applications
Alloy-Based Lightweight Verification for Aspect-Oriented Architecture
August 20-August 22
ISBN: 978-0-7695-3302-5
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 relation allogic. 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.
Index Terms:
AOP, Component-and-connector architecture, Alloy, Verification
Citation:
Naoyasu Ubayashi, Yuki Sato, Akihiro Sakai, Tetsuo Tamai, "Alloy-Based Lightweight Verification for Aspect-Oriented Architecture," sera, pp.171-178, 2008 Sixth International Conference on Software Engineering Research, Management and Applications, 2008