Aspect-oriented programming aims to enhancing concern modulization and integration of complex software systems, which arouses great interest for researchers and practitioners However, less attention has been paid to modeling and quality assurance at the early phase of aspect-oriented software development This paper proposes a modeling method based on an aspect extension of Object-Z The aspect extension provides means for observing behaviors of class schemas and depicting their interrelationships System functionality and other crosscutting concerns can be separately modeled, and a weaving mechanism systematically composes these models into a complete system model Our aspect-oriented modeling method enjoys good traceability for property analysis, and reusability for system specification.
