This paper discusses a formal and rigorous approach to the analysis of operator interaction with machines. It addresses the acute problem of detecting design errors in human-machine interaction and focuses on verifying the correctness of the interaction in complex and automated control systems. The paper describes a systematic methodology for evaluating whether the interface provides the necessary information about the machine, so as to enable the operator to perform a specified task successfully and unambiguously. It also addresses the adequacy of the information, provided to the user via training material (e.g., user manual), about the machine's behavior. The essentials of the methodology, which can be automated and applied to the verification of large systems, are illustrated by several examples and through a case study of pilot's interaction with an autopilot onboard a modern commercial aircraft. Running head: human-automation interaction. Key words: automation, modeling...