Systems Theoretic Process Analysis (STPA) is a powerful new hazard analysis method designed to go beyond traditional safety techniques - such as Fault Tree Analysis (FTA) - that overlook important causes of accidents like flawed requirements, dysfunctional component interactions, and software errors. While proving to be very effective on real systems, no formal structure has been defined for STPA and its application has been ad hoc with no rigorous procedures or model-based design tools. This paper defines a formal mathematical structure underlying STPA that can be used to rigorously identify potentially hazardous control actions in a system. A method for using these unsafe control actions to generate formal safety-critical, model-based system and software requirements is presented based on the underlying formal structure, as well as a way to detect conflicts between safety and other functional requirements during early development of the system.