Formal verification of human-automation interaction

Area of Science:

• Human-Computer Interaction
• Systems Engineering
• Automation and Control

Background:

• Detecting design errors in human-machine interaction is critical for complex automated systems.
• Ensuring operators have sufficient information for task success is a significant challenge.

Purpose of the Study:

• To present a formal and rigorous methodology for analyzing operator interaction with machines.
• To verify the correctness of human-automation interfaces in complex control systems.
• To evaluate the adequacy of information provided to operators through interfaces and training materials.

Main Methods:

• Developed a systematic methodology for evaluating information provision in human-machine interfaces.
• Applied the methodology to assess operator task performance and information adequacy.
• Utilized formal verification techniques for automated analysis of large systems.

Main Results:

• Demonstrated a method to systematically evaluate the information provided by machine interfaces.
• Illustrated the methodology's application through examples and a case study of pilot-autopilot interaction.
• Showcased the potential for automating the verification of human-automation interfaces.

Conclusions:

• The proposed methodology offers a formal approach to enhance the design and verification of human-automation interfaces.
• Formal verification can augment and improve the safety and effectiveness of operator interactions with automated systems.
• This approach is applicable to complex control systems, including aviation, to ensure operator success and system reliability.