document: Formal verification of human-automation interaction 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 to enable the operator to perform a specified task successfully and unambiguously . It also addresses the adequacy of information provided to the user via training materials -LRB- e.g. , user manual -RRB- 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 interaction with an autopilot aboard a modern commercial aircraft . The expected application of this methodology is an augmentation and enhancement , by formal verification , of human-automation interfaces
doc_bio_tags: B I O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B I I O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B O O O B I O O O O O O O O O O O O O O B I O O O O