Abstract
In this report we explore aspect-oriented modeling for UML 2.0 sequence diagrams. We ensure that the aspect weaving is semantics-based by using a formal trace model for sequence diagrams. A major challenge is to handle unbounded loops which produce infinite traces. We establish a systematic way to permutate and rewrite the original loop definition so that the weaving in many typical cases can be performed on a finite structure. We prove that it is always sufficient to consider a loop with upper bound relative to the pointcut definition to discover if the loop has infinitely repeating matches. A running example illustrates the approach and a prototype weaving tool is being implemented.