Architecture employs an iterative process that incrementally discovers inter-component interactions and explores local state spaces within each component. Thus, the architecture lazily constructs the behavior of the environment of a component in the target software system, and integrates the construction of the inter-component interactions with the model checking process itself, and hence, does not need to eagerly construct the interface process. Component-based state space reduction is applied during the exploration of the whole system. The architecture decomposes a target software system into a set of loosely coupled components where interactions between the components tend to be significantly simpler than interactions within each component. An iterative algorithm facilitates the component-based state space reduction, which is exponential, on the real large-scale software systems.