Global software development teams can collaboratively create Unified Modeling Language (UML) profiles, the primary mechanism for defining domain-specific variants on top of the UML. Usually, parts of UML profiles are separately elaborated to speed up the UML tailoring process, but at sometimes the parts built in parallel need to be brought together to construct a full UML profile. Although many model composition techniques have been proposed in the last decades, no one deals with issues required to combine UML profiles, e.g., matching and integration of UML stereotypes. Consequently, little is known about how to support the composition of UML profiles. Even worse, academia and industry have overlooked the elaboration of composition methods to support the integration of UML profiles, as well as the formal representation of such methods. This study, therefore, presents a composition mechanism, as well as introduces a lightweight UML extension to support the specification of composition relationships between UML profiles. The semantics of the extension and mechanism proposed was carefully represented in Alloy, a formal modeling language based on first-order logic. Then, we used the Alloy Analyzer to check the specification generated in Alloy for some specific algebraic properties, including idempotency, uniqueness, commutativity, and associativity.