Separation of concerns is one of the software engineering design principles that is getting more attention from practitioners and researchers in order to promote design and code reuse. Aspect-oriented programming is a maturing technique to enhance concern modulizalion and integration, which arouses great interest in both research society and software industry. However, less attention has been paid to modeling and quality assurance of aspect-oriented software development method. This paper proposes a formal aspect-oriented modeling language called AspectZ. and an aspect-oriented modeling method in AspectZ. The basic idea is to provide means for observing behaviors of Z schemas and depicting their interrelationships. and to provide ways for weaving interrelated schemas. Correctness of aspect weaving can he formally verified by the reasoning mechanisms of Z notation.
