Model Checking Human–Human Communication Protocols Using Task Models and Miscommunication Generation

Human–human communication is critical to safe operations in air transportation systems. For example, airlines develop and train pilots to use communication protocols designed to ensure that verbally communicated air traffic clearances are correctly executed by the pilots. Given the safety criticality of such interactions, these protocols should be designed to be robust to miscommunication. However, designers may not anticipate all of the different ways that miscommunication can occur. Thus, communication protocols can fail. This paper presents a method for evaluating human–human communication protocols using the enhanced operator function model with communications, which is a task analytic modeling formalism that can be used in model-checking formal verification analyses. In particular, a novel means of generating miscommunications from normative human–human communication protocols, instantiated as enhanced operator function models with communications, is introduced. An air transportation example is used to illustrate the power of the approach, where a protocol is iteratively evaluated and improved to make it robust for multiple miscommunications. Different versions of the application protocol are used to assess the scalability of the method. Results are discussed, and avenues of future research are explored.