In this paper we present a formal methodology and an algorithmic procedure for constructing human-automation interfaces and corresponding user-manuals. Our focus is the information provided to the user about the behavior of the underlying machine, rather than the graphical and layout features of the interface itself. Our approach involves a systematic reduction of the behavioral model of the machine, as well as systematic abstraction of information that displayed in the inter - face. This reduction procedure satisfies two requirements: First, the interface must be correct so as not to cause mode confusion that may lead the user to per - form incorrect actions. Secondly, the interface must be as simple as possible and not include any unnecessary information. The algorithm for generating such inter - faces can be automated, and a preliminary software system for its implementation has been developed.