Abstract: Aspect-Oriented Programming (AOP) can effectively solve the code-tangling and code-scattering caused by crosscutting attributes; however, much work is presented on the programming and the implementation phase, and little has addressed the early model stages. A research is conducted on the requirements engineering phase of software by using AOP technology. First in the requirements analysis phase, the functional requirements and non-functional requirements are identified by the separation of concerns, and the functional requirements with components and the non-functional requirements with aspects are realized. Then the components and aspects are represented by combining with the formal language Aspect-Z which has the characteristics of accurate description. As actions accompany conflicts while two or more aspects affect the same joint point synchronously, a method is proposed to solve by defining aspects' priority level. In the end, the properties and attributes of the described requirements are deduced by the theorem proving method, so as to achieve the purpose of formal verification of Aspect-Z specifications. Finally, an application example is given.

Key words: AOP, requirements analysis, Aspect-Z, formal verifications