La programmation par aspects s'avère bien adaptée aux processus de développement incrémentaux qui nécessitent la prise en compte des préoccupations transverses et l'ajout de fonctionnalités auxiliaires. Pour satisfaire aux besoins de ces processus, nous proposons une méthodologie de modélisation et de vérification des systèmes par aspects. Notre approche de vérification a deux objectifs : assurer que l'introduction d'un nouvel aspect ne compromet pas la correction du système initial, détecter les problèmes liés à la composition d'aspects dont l'exécution peut s'avérer conflictuelle. Cet article présente notre profil de modélisation AspectUML, ainsi que la traduction de ses modèles en réseaux de Petri colorés. Cette traduction confère à Aspect-UML une sémantique sur laquelle s'appuyer pour la vérification, par modelchecking et analyse, de la composition et du tissage des aspects dans un système de base.