Abstract: Aspect-oriented modeling technique can identify and validate crosscutting concerns in the early stages of the software development. This paper presents an Petri net-based approach for aspect-oriented modeling so as to solve the problems of ambiguity, contradiction, omission usually found in the textual form of use case descriptions. In addition, the mapping rules to derive an aspect-oriented Petri net from the use case diagram, which is analyzed by temporal logic, are proposed to formalize the modeling and analysis approach. Finally, a case is provided to demonstrate and analyze the modeling method.