Design Vulnerabilities and Design Assumptions in Automated Systems: The Case of the B737 MAX Original MCAS Design

In this paper, we demonstrate how formal modeling of human-machine systems can uncover design vulnerabilities. Two fatal accidents involving the Boeing B737 MAX raised substantial safety concerns about the aircraft’s design and led to the worldwide grounding of the MAX. These accidents involved design vulnerabilities, design assumptions about human performance that proved unwarranted, and an operational context that differed from what the designers assumed. The two accidents also involved the operation of the Maneuvering Characteristics Augmentation System (MCAS) that was introduced into the pitch trim system of the B737 MAX. We use the case of the MAX to show that by building a formal model of this system including MCAS and examining it with an analytical methodology, the vulnerabilities in the design become visible. By comparing this model with a model of the MAX’s predecessor, the B737NG, we highlight discrepancies between the design assumptions about how pilots would act when faced with system failures and the crew actions observed in the first accident. Using a formal approach to describing human interaction with automated systems to identify design vulnerabilities can be productively employed in the design of automated systems, regulatory assessment, and accident investigation.