Recent years have seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software, systems. Success in scaling these techniques to be practical for realistic software systems has met with a number of obstacles, such as exponentially-sized state spaces and the problem of constructing finite-state system models for analysis. We describe an automatable approach for building finite-state models of partially defined software systems that are amenable to model checking using existing tools. It enables the application of model checking techniques to individual system components taking into account assumptions about the behavior of the environment in which the components will execute. We illustrate the application of the approach by validating and verifying properties of a reusable parameterized programming framework.