  Architecture patterns capture architectural design experience and provide
abstract solutions to recurring architectural design problems. They consist of
a description of component types and restrict component connection and
activation. Therefore, they guarantee some desired properties for architectures
employing the pattern. Unfortunately, most documented patterns do not provide a
formal guarantee of whether their specification indeed leads to the desired
guarantee. Failure in doing so, however, might lead to wrong architectures,
i.e., architectures wrongly supposed to show certain desired properties. Since
architectures, in general, have a high impact on the quality of the resulting
system and architectural flaws are only difficult, if not to say impossible, to
repair, this may lead to badly reparable quality issues in the resulting
system. To address this problem, we propose an approach based on model checking
to verify pattern specifications w.r.t. their guarantees. In the following we
apply the approach to three well-known patterns for dynamic architectures: the
Singleton, the Model-View-Controller, and the Broker pattern. Thereby, we
discovered ambiguities and missing constraints for all three specifications.
Thus, we conclude that verifying patterns of dynamic architectures using model
checking is feasible and useful to discover ambiguities and flaws in pattern
specifications.
