Using Model Checking to Validate Style-Specific Architectural Refactoring Patterns
Presented at 31st IEEE Software Engineering Workshop, Baltimore, Maryland, March 2007
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.