Automatic verification techniques, which analyze all processes at once, typically do not scale well for large, complex concurrent software systems because of the theoretic barrier – PSPACE hard complexity in worst case. In this paper, we present our tool named ARCATS (Architecture Refactoring and Compositional Analysis Tool Suite). ARCATS consists a set of tools to combat state explosion in a divideand- conquer, hierarchical fashion. These tools can be applied in a multi-phased manner until a balance between intractability and feasibility is reached. We build these tools to seek out perfect combinations for analyzing large-scale, complex software system with state space growth carefully controlled.