Using Model Checking to Validate Style-Specific Architectural Refactoring Patterns

When developing a new domain-specific architectural style, there can be uncertainty about the feasibility of using that style. In particular, the HADES architectural style contains refactoring patterns intended to remove undesirable 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 input 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.