In this paper we propose a formal approach and methodology for analysis and generation of human-machine interfaces, with special emphasis on human-automation interaction. Our approach focuses on the information content of the interface—that is, on “what should be presented”—rather than on the form and layout of the graphical user interface (“how it should be presented”). The methodology is guided by two criteria: First and foremost, the interface must be correct. That is, given the interface indications and all related information (e.g., user manuals, training material, etc.), the user must be able to successfully perform the specified tasks. Second, the interface and related information should be succinct—that is, the amount of information (e.g., mode indications, mode buttons, parameter settings, etc.) presented to the user should be reduced ted) to the minimum necessary. The foundation of our approach is on of information abstraction. We argue that in terms of the inf...