Abstract: Aspect-oriented programming is proposed as a technique for improving separation of concerns in software development.However,less attention is paid to modeling and quality assurance at early stages of aspect-oriented software development.This paper proposes an aspect-oriented formal modeling language based on Object-Z and its corresponding modeling method.Aspect specification provides means to observe behaviors of class schema and aspect schema,and to describe their interrelationship.The weaving mechanism sy...