The NASA-Task Load Index (TLX) and its variants are the most widely used measures of mental workload. However, an increasing body of literature suggests that there are critical problems with this measure. This includes confusing elements of its design that may bias human response or result in administrator error, inconsistent dimensions, limitations in how dimensions are weighted when computing overall workload scores, multicollinearity between dimensions biasing results, and fundamental measurement theory problems that impact the meaningfulness of computed overall workload. This article provides an overview of these problems. We then make recommendations for addressing them through changes in experimental practice and design, as well as practices that can be used by researchers in the intervening period. We recommend that researchers assess the appropriateness of the TLX for every study, combine its use with other measures, analyze dimensions separately instead of overall workload, and use within-subject designs when possible. Finally, we call on the research community to standardize NASA-TLX versions and instructions, audit existing TLX results, and investigate methods to address existential issues.

Human users are increasingly recognized as a vector of cybersecurity attack. One problem that contributes to this condition is the growing complexity of digital tools. Such complexity can make it difficult for users to understand how tools work and how their actions will impact security. This work sought to answer the research question: Can mental modeling analyses (from human factors engineering and human-automation interaction) be developed to effectively discover cybersecurity risks? To answer this, we extend mental models with cybersecurity-specific concepts. The resulting models are then incorporated into model checking analyses (an automated approach to formal verification) to discover if and when mismatches between human mental models and systems can cause security failures. We evaluated our approach by successfully applying it to a case study regarding the security configuration of a popular cloud data storage service. We ultimately discuss the results of this analysis and outline future research possibilities.

Human error is often associated with system failures. The complexity of human-automation interaction can make it difficult to anticipate what errors can occur and how they contribute to failures. Previous research has shown that task analytic behavior modeling with the enhanced operator function model and the cognitive reliability analysis method (CREAM) can be combined with statistical model checking to make predictions about human error rates, their stochastic impact on system failures, and the effect of negative transfer of design changes on these predictions. These efforts were successful, but the validation studies used artificial examples with limited data. Predictions also slightly overestimated error rates. This article addresses these deficiencies by conducting a validation study based on the prescription order entry interface of the OpenEMR electronic medical record. As part of this, we explored how prediction accuracy for the OpenEMR application changed based on the inclusion/exclusion of planning errors: errors based on people’s ability to formulate task plans, which we hypothesized contributed to error rate overestimation. Results found that our method’s predictions aligned with those observed in the experiment, especially when planning errors were excluded. Negative transfer conditions did not manifest significant differences in error rates experimentally or in model predictions. These results suggest that negative transfer’s impact on human–computer interaction may be overstated in the literature. Finally, higher error rates were observed between the original OpenEMR prescription order entry interface compared to an alternative that we tested. We highly suggest that OpenEMR adopt the alternative.

In the burgeoning field of human-AI interaction, trust emerges as a cornerstone because many think that it is critical to the effectiveness of collaboration and the acceptance of AI systems. Traditional methods of assessing trust have predominantly relied on self-reported measures, requiring participants to articulate their perceptions and attitudes through questionnaires. However, these explicit methods may not fully capture the nuanced dynamics of trust, especially in real-time and complex interaction environments. This paper introduces an innovative approach to evaluating trust in human-AI teams, pivoting from the conventional reliance on verbal or written feedback to analyzing gameplay behaviors as implicit indicators of trust levels. Utilizing the Overcooked-AI environment, our study explores how participants’ interactions with AI agents of varying performance levels can reveal underlying trust mechanisms without a single query posed to the human players. This approach not only bypasses the efficiency challenges posed by repetitive and lengthy trust assessment methods, but also provides insights comparable to them. We highlight the potential of non-verbal cues and action patterns as reliable trust indicators by comparing the predictive accuracies of questionnaire-based models with those derived from gameplay behavior analysis. Furthermore, our findings suggest that these implicit measures can be integrated into adaptive systems and algorithms for real-time trust calibration in human-agent teaming settings. This shift towards an action-oriented trust assessment challenges existing paradigms and opens new avenues for understanding and enhancing human-AI collaboration.

Modern software systems are deployed in a highly dynamic, uncertain environment. Ideally, a system that is robust should be capable of establishing its most critical requirements even in the presence of possible deviations in the environment. We propose a technique called behavioral robustification, which involves systematically and rigorously improving the robustness of a design against potential deviations. Given behavioral models of a system and its environment, along with a set of user-specified deviations, our robustification method produces a redesign that is capable of satisfying a desired property even when the environment exhibits those deviations. In particular, we describe how the robustification problem can be formulated as a multi-objective optimization problem, where the goal is to restrict the deviating environment from causing a violation of a desired property, while maximizing the amount of existing functionality and minimizing the cost of changes to the original design. We demonstrate the effectiveness of our approach on case studies involving the robustness of an electronic voting machine and safety-critical interfaces.

Previous research has shown how statistical model checking can be used with human task behavior modeling and human reliability analysis to make realistic predictions about human errors and error rates. However, these efforts have not accounted for the impact that design changes can have on human reliability. In this research, we address this deficiency by using similarity theory from human cognitive modeling. This replicates how negative transfer can cause people to perform old task behaviors on modified systems. We present details about how this approach was realized with the PRISM model checker and the enhanced operator function model. We report results of a validation exercise using an application from the literature. We discuss the implications of our results and describe future research.

Mental workload extremes are associated with poor human performance and safety problems across safety critical domains. Mental workload is a complex, difficult-to-predict phenomenon, where issues may only arise due to concurrency between resource-conflicting tasks. This research addresses this deficiency by presenting a novel method for using model checking (for performing formal proofs about concurrent systems) to predict mental workload. Our method combines multiple resource theory and formal methods based on hierarchical task analysis to identify mental workload extremes in a complex system. This paper presents this method and shows preliminary validation using a texting and driving task. Implications of our results and future research are discussed.

Human mental workload can profoundly impact human performance and is thus an important consideration in the design and operation of many systems. The standard method for assessing human mental workload is the NASA Task Load Index (NASA-TLX). This involves a human operator subjectively rating a task based on six dimensions. These dimensions are combined into a single workload score using one of two methods: scaling and summing the dimensions (where scales are derived from a paired comparisons procedure) or averaging dimensions together. Despite its widespread use, the level of measurement of NASA-TLX's dimensions and its computed workload score has not been investigated. Additionally, nobody has researched whether NASA-TLX's two approaches for computing overall workload are mathematically meaningful with respect to the constituent dimensions' levels of measurement. This is a serious deficiency. Knowing what the level of measurement is for NASA-TLX scores will determine what mathematics can be meaningfully applied to them. Furthermore, if NASA-TLX workload syntheses are mathematically meaningless, then the measure lacks construct validity. The research presented in this article used a previously developed method to evaluate the level of measurement of NASA-TLX workload and its dimensions. Results show that the dimensions can, in most situations, be treated as interval in population analyses and ordinal for individuals. Our results also suggest that the methods for combining dimensions into workload scores are meaningless. We recommend that analysts evaluate the dimensions of NASA-TLX without combining them.

Situation awareness (SA), a measure of how well a person understands the situation, is frequently used to evaluate the safety and effectiveness of critical systems that depend on human behavior. While there are objective ways of measuring SA, subjective assessments, such as the SA rating technique (SART), are still widely used. However, it is not clear what the level of measurement is for SART-measured SA or its constituent dimensions This is a significant gap because the level of measurement determines what mathematics and statistics can be meaningfully used to synthesize and evaluate measures. This research uses a previously developed method for determining the level of measurement of psychometric ratings to evaluate the level of measurement of SART and its elements. Results show that all of the dimensions of SA can be treated as interval in most situations, but that each is on a separate interval scale. This result casts doubt on the validity of the formula SART uses to compute SA from its subcomponents. We ultimately discuss our results and explore future research directions.

A forcing function is an intervention for constraining human behavior. However, the literature describing forcing functions provides little guidance for when and how to apply forcing functions or their associated trade-offs. In this paper, we address these shortcomings by introducing a novel taxonomy of forcing functions. This taxonomy extends the previous methods in four ways. First, it identifies two levels of forcing function solidity: hard forcing functions, which explicitly enforce constraints through the system, and soft forcing functions, which convey or communicate constraints. Second, each solidity level is decomposed into specific types. Third, the taxonomy hierarchically ranks forcing function solidities and types based on trade-offs of constraint and resilience. Fourth, for hard forcing functions, our taxonomy offers formal guidance for identifying the minimally constraining intervention that will prevent a specific error from occurring. We validated the ability of our method to identify effective error interventions by applying it to systems with known errors from the literature. We then compared the solutions offered by our method to known, effective interventions. We discuss our results and offer suggestions for further developments in future research.

User-centered design (UCD) is an approach for creating human-machine interfaces that are usable and support the human operator's tasks. UCD can be challenging because designers can fail to account for human-machine interactions that occur due to the concurrency between the human and the other system elements. Formal methods are tools that enable analysts to consider all of the possible system interactions using a combination of formal modeling, specification, and proof-based verification. However, creating formal interface design models can be extremely difficult. This work describes a method that supports UCD by automatically generating formal designs of human-machine interface behavior from task-analytic models. The resulting interface design will always support the behavior captured in the task model. This paper describes the method and demonstrates its capabilities with three case studies: a light switch, a vending machine, and a patient-controlled analgesia pump. The produced designs are validated with formal verifications to prove that they support their associated tasks. Results and future research are discussed.

Judgment analysis (JA) is a technique for modeling and interpreting human judgments that is usually based on multiple linear regression. However, the linear assumptions inherent to this approach can be limiting for modeling both the human judgments and the environmental criterion. This paper addresses this by introducing a formulation of JA based on large memory storage and retrieval (LAMSTAR) artificial neural networks. We describe our LAMSTAR network JA process and use it to analyze data from an air traffic control conflict prediction task. These results are compared with those of a traditional regression-based lens model analysis. We found that the LAMSTAR-based JA did a better job of capturing human judgment, while the regression-based model was more appropriate for the criterion. This suggest that the LAMSTAR-based JA approach has utility when human judgments are not well represented by a linear model. We discuss our results with respect to both the specific application we evaluated as well as meta-analyses of the JA literature. We also explore avenues for future research.

The ability of people to hear and respond to auditory medical alarms is critical to the health and safety of patients. Unfortunately, concurrently sounding alarms can perceptually interact in ways that mask one or more of them: making them impossible to hear. Because masking may only occur in extremely specific and/or rare situations, experimental evaluation techniques are insufficient for detecting masking in all of the potential alarm configurations used in medicine. Thus, a real need exists for computational methods capable of determining if masking exists in medical alarm configurations before they are deployed. In this paper, we present such a method. Using a combination of formal modeling, psychoacoustic modeling, temporal logic specification, and model checking, our method is able to prove whether a modeled of a configuration of alarms can interact in ways that produce masking. This paper provides the motivation for this method, presents its details, describes its implementation, demonstrates its power with a case study, and outlines future work.

In complex human-machine systems, unforeseen failures in the interaction between human agents, automation and the environment provide an important contribution to incidents and accidents. The complexity of many systems precludes a designer from foreseeing all possible states of interaction. Formal verification methods are explored as a means of making human-machine systems more robust against failures arising from these unforeseen interactions. For these methods, a analytic model of the operator task is combined with a formal model of the system (automation), and, using model checking tools, a formal verification of the interaction is performed. Validity of the results, however, does require a sufficient correspondence between the model and the actual system. To validate this correspondence, this study explores an approach where the predictions from a formal model are compared to behavior of the human-machine system. The Paparazzi UAV ground control station is used as a test case, and a framework was created to automatically play back results from the formal verification tool to the UAV ground control simulation. The results show a good correspondence between the actual system and the model results, even if the model is by necessity a simplified description of actual system behavior. A remaining problem is creating enough variation in verification tool traces to properly test the correspondence between the formal model and the system.

Human-automation interaction (HAI) is often a contributor to failures in complex systems. This is frequently due to system interactions that were not anticipated by designers and analysts. Model checking is a method of formal verification analysis that automatically proves whether or not a formal system model adheres to desirable specification properties. Task analytic models can be included in formal system models to allow HAI to be evaluated with model checking. However, previous work in this area has required analysts to manually formulate the properties to check. Such a practice can be prone to analyst error and oversight which can result in unexpected dangerous HAI conditions not being discovered. To address this, this paper presents a method for automatically generating specification properties from task models that enables analysts to use formal verification to check for system HAI problems they may not have anticipated. This paper describes the design and implementation of the method. An example (a pilot performing a before landing checklist) is presented to illustrate its utility. Limitations of this approach and future research directions are discussed.

Physician handoff of care is a mechanism for transferring patient information, responsibility, and authority from one set of caregivers to another. At shift change at a hospital, residents going off shift handoff patients to those coming on shift. There are limited handoff of care tools that facilitate the handover process by condensing patient information in reports that can be referenced during the handoff of care and used during patient care as cognitive artifacts. This effort works to address information, data entry and reporting requirements for a resident handoff of care tool that would support transfer of information as well as patient care.

The purpose of the framework introduced here is to support the development of evaluation scenarios that are capable of assessing system level performance while considering the system, the humans that interact with it, and the environment. The following five step framework is presented and applied to a pilot self separation task: 1) identify entities critical to system design, development, and operation and define their goals and properties as they relate to the system being studied; 2) define a subset of functionality for evaluation (define an execution sequence); 3) map entity properties to the execution sequence to identify independent variables; 4) translate entity goals into a set of system goals that can be used to identify dependent measures; and 5) iterate through each step to ensure the models produced are internally consistent.

Human-automation interaction, including erroneous human behavior, is a factor in the failure of complex, safety-critical systems. This paper presents a method for automatically generating formal task analytic models encompassing both erroneous and normative human behavior from normative task models, where the misapplication of strategic knowledge is used to generate erroneous behavior. Resulting models can be automatically incorporated into larger formal system models so that safety properties can be formally verified with a model checker. This allows analysts to prove that a human-automation interactive system (as represented by the formal model) will or will not satisfy safety properties with both normative and generated erroneous human behavior. Benchmarks are reported that illustrate how this method scales. The method is then illustrated with a case study: the programming of a patient-controlled analgesia pump. In this example, a problem resulting from a generated erroneous human behavior is discovered. The method is further employed to evaluate the effectiveness of different solutions to the discovered problem. The results and future research directions are discussed.

Failures in complex systems controlled by human operators can be difficult to anticipate because of unexpected interactions between the elements that compose the system, including human-automation interaction (HAI). HAI analyses would benefit from techniques that support investigating the possible combinations of system conditions and HAIs that might result in failures. Formal verification is a powerful technique used to mathematically prove that an appropriately scaled model of a system does or does not exhibit desirable properties. This paper discusses how formal verification has been used to evaluate HAI. It has been used to evaluate human-automation interfaces for usability properties and to find potential mode confusion. It has also been used to evaluate system safety properties in light of formally modeled task analytic human behavior. While capable of providing insights into problems associated with HAI, formal verification does not scale as well as other techniques such as simulation. However, advances in formal verification continue to address this problem, and approaches that allow it to complement more traditional analysis methods can potentially avoid this limitation.

Breakdowns in complex systems often occur as a result of system elements interacting in ways unanticipated by analysts or designers. The use of task behavior as part of a larger, formal system model is potentially useful for analyzing such problems because it allows the ramifications of different human behaviors to be verified in relation to other aspects of the system. A component of task behavior largely overlooked to date is the role of human-human interaction, particularly human-human communication in complex human-computer systems. We are developing a multi-method approach based on extending the Enhanced Operator Function Model language to address human agent communications (EOFMC). This approach includes analyses via theorem proving and future support for model checking linked through the EOFMC top level XML description. Herein, we consider an aviation scenario in which an air traffic controller needs a flight crew to change the heading for spacing. Although this example, at first glance, seems to be one simple task, on closer inspection we find that it involves local human-human communication, remote human-human communication, multi-party communications, communication protocols, and human-automation interaction. We show how all these varied communications can be handled within the context of EOFMC.

Human-automation interaction, including erroneous human behavior, is a factor in the failure of complex, safety-critical systems. This paper presents a method for automatically generating task analytic models encompassing both erroneous and normative human behavior from normative task models by manipulating modeled strategic knowledge. Resulting models can be automatically translated into larger formal system models so that safety properties can be formally verified with a model checker. This allows analysts to prove that a human automation-interactive system (as represented by the formal model) will or will not satisfy safety properties with both normative and generated erroneous human behavior. This method is illustrated with a case study: the programming of a patient-controlled analgesia pump. In this example, a problem resulting from a generated erroneous human behavior is discovered and a potential solutions is explored. Future research directions are discussed.

Formal methods are typically used in the analysis of complex system components that can be described as “automated” (digital circuits, devices, protocols, and software). Human-automation interaction has been linked to system failure, where problems stem from human operators interacting with an automated system via its controls and information displays. As part of the process of designing and analyzing human-automation interaction, human factors engineers use task analytic models to capture the descriptive and normative human operator behavior. In order to support the integration of task analyses into the formal verification of larger system models, we have developed the enhanced operator function model (EOFM) as an Extensible Markup Language-based, platform- and analysis-independent language for describing task analytic models. We present the formal syntax and semantics of the EOFM and an automated process for translating an instantiated EOFM into the model checking language Symbolic Analysis Laboratory. We present an evaluation of the scalability of the translation algorithm. We then present an automobile cruise control example to illustrate how an instantiated EOFM can be integrated into a larger system model that includes environmental features and the human operator's mission. The system model is verified using model checking in order to analyze a potentially hazardous situation related to the human-automation interaction.

Model checking is a type of automated formal verification that searches a system model's entire state space in order to mathematically prove that the system does or does not meet desired properties. An output of most model checkers is a counterexample: an execution trace illustrating exactly how a specification was violated. In most analysis environments, this output is a list of the model variables and their values at each step in the execution trace. We have developed a language for modeling human task behavior and an automated method which translates instantiated models into a formal system model implemented in the language of the Symbolic Analysis Laboratory (SAL). This allows us to use model checking formal verification to evaluate human-automation interaction. In this paper we present an operational concept and design showing how our task modeling visual notation and system modeling architecture can be exploited to visualize counterexamples produced by SAL. We illustrate the use of our design with a model related to the operation of an automobile with a simple cruise control.

Task analytic models are extremely useful for human factors and systems engineers. Unfortunately, there is no standard language for describing task models. We present an XML-based task analytic modeling language. The language incorporates features from operator function model and extends them with additional task sequencing options and conditional constraints. This language's use is illustrated via a radio alarm clock example. In addition, parsing, visualization, and development tools are discussed.

Stevens' power law links the magnitude of a physical stimulus to its perceived internal intensity via a psychophysical power function. Because of the law's sensitivity to the procedure used to collect its data, its failure to manifest itself at the individual level, its manifestation in non-sensory modalities, and the difficulty associated with rating stimuli on a ratio scale, many have speculated that the power law is a product of the experimental procedure Stevens used. This work tested this hypothesis by reproducing one of Stevens' original power law experiments (using different pressure levels of a 1 kHz tone) in which 52 data series were generated from a computerized process that simulated Stevens' experimental procedure. However, instead of generating ratio data for each magnitude estimate, random ordinal data were generated. When a power function was fitted to these data using the same procedure utilized by Stevens, it fit with an adjusted R2of 0.997, while generating the same psychophysical model. This indicates that Stevens' assumption that participants make magnitude estimates on a ratio scale is not necessary to collect power law data. Thus, Stevens' power law is likely a product of Stevens' experimental procedure.

Spatial awareness is important in domains where safety hinges on human operators keeping track of the relative locations of objects in their environments. While a variety of subjective and judgment-based measures have been used to evaluate spatial awareness, none have probed all three of its levels: 1) identification of environmental objects, 2) their current locations relative to the operator, and 3) their relative positions over time. This work compares new judgment based measures of spatial awareness that probe all three levels of spatial awareness to conventional subjective measures. In the evaluation of 14 configurations of Synthetic Vision Systems head down displays (7 terrain textures and 2 Fields of View (FOVs)), 18 pilots made 4 types of judgments (relative angle, distance, height, and a beam time) regarding the location of terrain points displayed in 112 5-second, non-interactive simulations. They also provided subjective awareness and SA-SWORD measures. ANOVA analyses revealed that comparable results were found between display configurations that produced the minimum error in judgments and those that received the highest subjective ratings. However, none of the subjective measures were correlated with judgment error. Thus, given that the judgment based measures were explicitly designed to measure all three levels of spatial awareness, the subjective measures may not be measuring spatial awareness.

The evaluation of human-centered systems can be performed using a variety of different methodologies. This paper describes a human-centered systems' evaluation methodology where participants watch 5-second non-interactive videos of a system in operation before supplying judgments and subjective measures based on the information conveyed in the videos. This methodology was used to evaluate the ability of different textures and fields of view to convey spatial awareness in synthetic vision systems (SVS) displays. It produced significant results for both judgment based and subjective measures. This method is compared to other methods commonly used to evaluate SVS displays based on cost, the amount of experimental time required, experimental flexibility, and the type of data provided.

There is a lack of educational technology to support cognitive systems engineering topics such as models of human performance in dynamic environments. This paper describes the Cognitive Systems Engineering Educational Software (CSEES) system, an integrated toolset designed to facilitate curricula related to human judgment and decision-making performance modeling and evaluation. CSEES provides students with the means to generate and analyze performance data using multiple methods. It also includes documentation and tutorials. Its flexible design facilitates adding new judgment and decision making task environments. The paper describes the initial system implementation as a Microsoft Excel add-on, a preliminary evaluation as part of a graduate engineering course, and planned future work.