AspectJ is an aspect-oriented extension of the Java language that enables a modular implementation of crosscutting concerns. Despite this, aspects lack support for formal specification and verification. This paper expresses the base class and some related aspects of AspectJ model in B notation. It aims to benefit from proof obligations generated by B tools to ensure the correctness of AspectJ component composition. Static crosscuts of aspects are guaranteed by proof obligations of relation clauses between B abstract machines and dynamic crosscuts are proved by proof obligations of B refinement machines. This approach is illustrated by verifying a simple example. © 2007 IEEE.

Thuan T.N., Ha N.V.

537.pdf    Gửi cho bạn bè

Từ khóa : Formal logic; Java programming language; Mechanics; Software engineering; Technology; Abstract machines; Asia Pacific; Aspect-J; Aspect-oriented; Base class; component composition; Crosscutting concerns; Formal specification and verification; Modular implementation; proof obligations; Computer software