When developing a new domain-specific architectural style, there can be uncertainty about the feasibility of us- ing that style. In particular, the HADES architectural style contains refactoring patterns intended to remove undesir- able scheduling features such as deadlock and livelock, but these patterns have not yet been fully validated. We report on the translation between the HADES structure and the in- put languages for two popular model checkers (SPIN and NuSMV) to help validate these patterns. We found model checking to be a valuable asset in confirming the presence of undesirable features.