Models of Human-Automation Systems: Initial Analysis of the Boeing 737MAX Design

We describe a formal approach to identifying human factor design vulnerabilities and usability concerns in the context of automated control systems. We present an initial analysis of the design of the B737MAX that has suffered two fatal accidents. We highlight two main design vulnerabilities and one usability concern. Key formal generic properties used to identify these vulnerabilities and usability concerns are defined. These generic properties, and others referenced in this paper, can be applied to the analysis of any human-automation system.