Precise notations have been developed to specify unambiguous requirements, and ensure that all cases of appropriate system behavior are considered and documented. Using one such notation, we have developed techniques to automatically analyze software artifacts at early stages of the software development life cycle. We use model checking as our verification technique because it can be fully automated and can check properties of large systems. This paper describes model checking and summarizes our efforts to use it to analyze software requirements and designs. We prove that requirements model system safety properties and that designs model consistency properties derived from requirements by creating abstractions of these software artifacts and using model checking to determine if the abstractions are models of the properties. We present results from a case study in which we analyzed the requirements and design of a small but realistic system.