# Survey of Human Models for Verification of Human-Machine Systems

Timothy E. Wang Alessandro Pinto Raytheon Technologies Research Center, East
Hartford, CT, USA<EMAIL_ADDRESS>Technologies Research Center,
Berkeley, CA, USA<EMAIL_ADDRESS>
###### Abstract

We survey the landscape of human operator modeling ranging from the early
cognitive models developed in artificial intelligence to more recent formal
task models developed for model-checking of human machine interactions. We
review human performance modeling and human factors studies in the context of
aviation, and models of how the pilot interacts with automation in the
cockpit. The purpose of the survey is to assess the applicability of available
state-of-the-art models of the human operators for the design, verification
and validation of future safety-critical aviation systems that exhibit higher-
level of autonomy, but still require human operators in the loop. These
systems include the single-pilot aircraft and NextGen air traffic management.
We discuss the gaps in existing models and propose future research to address
them.

###### Index Terms:

##  I Introduction

The development of increasingly capable Artificial Intelligence (AI) and
Machine Learning (ML) techniques, is inspiring both industry and academia to
build systems that automate the execution of certain tasks in a variety of
applications. These systems do not replace humans, but rather help to simplify
operations and, at minimum, the human is still responsible to provide goals to
the intelligent agents that execute these tasks. Moreover, humans are involved
in being part of the execution process by providing information that
automation cannot infer reliably, or by making decisions whose consequences
cannot be accurately predicted by the autonomous systems. Thus, at least for
the foreseeable future, autonomous systems will be required to interact with
humans, collaborating and complementing each other towards delivering systems
that can effectively operate in complex environments. The design of these
human-machine systems (HMS) challenges the adequacy of current development
processes especially when the application domain is safety critical, such as
commercial aviation. These applications require a high-level of assurance and
demand for evidence that the closed-loop system satisfies stringent safety and
performance requirements.

Verification and Validation (V&V) are critical steps in a high-assurance
design process. A V&V methodology (Figure 1) defines the set of tools and
techniques to arrive at a safety argument, including the functional view of
the system, the modeling activities, and how to use their results. Several
techniques can be used to generate evidence such as simulation, formal
verification, and field-testing. While the latter is necessary at some point
in the verification process, it involves prototyping and testing campaigns
that are expensive. Field-testing alone becomes impractical for autonomous
systems due to the large number of scenarios required to achieve coverage. For
example, it is predicted that an autonomous car would need to drive in
realistic conditions for billions of miles before reaching confidence on its
safety statistics[1]. Simulation and formal verification are therefore
appealing alternatives aiming at reducing the amount of field-testing while at
the same time providing confidence on safety and performance. These techniques
rely on models that are machine-interpretable and that can be used in a
systematic exploration of plausible scenarios to find errors. These models
must include three sub-components (Figure 1): the system comprising one or
multiple machines, the environment, and the human. Developing these models is
hard in general. Models of machines can be built by engineers, as they are the
subject of the design activity. The environment and the human models are
typically not readily available and require substantial development effort.
Among these two, the environment model captures the physical space in which
the system operates and can be developed by leveraging knowledge of the
application domain. However, the development of capability, performance, and
behavioral models of humans is considerably harder, as it must account for
behavioral, neurological, sociological, psychological, and systems aspects
that are difficult to formalize.

Given the importance of a virtual engineering platform for autonomy
applications, and the complexity associated with building models of humans,
this survey focuses on identifying the major currents and gaps in the ocean of
knowledge about human modeling for the specification, design, verification and
validation of HMS. We survey both simulation and formal models for the major
functions of a human decision cycle including perception, cognition, decision-
making, and action, and we also provide extensive background on performance
and error models.

Figure 1: Typical framework for design, analysis and verification of human-
machine systems from functional decomposition to safety arguments.

###  I-A Overview of Human Models Surveyed

The human models surveyed in this paper span all 3 of these types:
_descriptive_ , _computational_ , and _formal_. Descriptive models represent
the quality of the human behavior without producing any quantitative outputs.
Computational models, in contrast, can be simulated or executed to produce
quantitative predictions about the performance of the HMS. Formal models are
rigorous mathematical descriptions that can be used for formal analysis.
Formal analysis differs from computational analysis in the sense that the
former generates proofs that guarantee that certain properties of the system
are satisfied under all modeled environment, while the latter can be used to
test the system in a given scenario or sets of scenarios. Formal methods are
used in analysis, but they can also be used for synthesizing systems with
given property, thereby enabling correct-by-construction design.

In terms of specification language, descriptive models are typically given in
a natural language such as English. Computational and formal models are
specified using a rich variety of mathematical and/or formal languages: static
equations such as linear and nonlinear equations including neural networks,
dynamical equations such as differential equations, Markov decision processes,
Kalman filters, statistical models such as Bayesian nets, Structured Equation
Models, state-machines such as FSM, Petri-nets, programming languages as in
cognitive architectures, and logic such as modal predicate logic.

A typical property to be verified is whether the HMS satisfies certain
performance or safety constraints. Oftentimes, performance models are
constructed using certain hidden states or latent variables of a human such as
boredom. For that reason, we also survey the models that are based on those
hidden states in the context of using them for design and verification.

The survey starts in Section II by discussing some of the fundamental concepts
of human modeling (see the human box in Figure 1) that are related to the OODA
loop [2]. These “first principles of human”, come from scientific studies of
human behaviors and cognition from fields such as psychology, sociology and
artificial intelligence. This is followed by Section III with an introduction
to various hidden states modelled in the human factors field along with a
discussion of the various “failure modes” of a human. This is motivated by our
system-theoretic interpretation of the human, with inputs and outputs,
unobservable hidden states, and faults. In Section IV, we review formal
models. The notion of an epistemic model is introduced and some of the
challenges in formally verifying epistemic models are discussed. In Section V
we review various computational or simulation models used in the analysis and
verification of human-machine systems including integrated frameworks for the
simulation of performance and behavior of a pilot in the cockpit. Finally, we
conclude this paper with a set of recommendations on the research and
development efforts needed to build a unified framework for modeling and V&V
of future human-autonomy systems. In summary, the models survey in this paper
are categorized in Table I.

TABLE I: Summary of surveyed models Category |  Models Surveyed
---|---
Application |  human-aviation systems
Capabilities |  visual and perception, cognition, decision making, actuation
Specification language |  natural language, static equations, dynamic equations, stochastic equations, logic, programs, state machines
Verification techniques |  simulation, formal verification
Hidden states |  workload, trust, situational awareness, boredom, complacency, vigilance

###  I-B Related Work

There are prior works in the literature which also survey human modeling for
the purpose of verifying human-machine interaction.

For example, in [3], Bolton et al. provides perhaps the earliest known surveys
on human models for formal verification of human-computer interaction (HCI).
In addition, Weyers et al. in their book [4] provide a comprehensive
collection of works on formal methods usage in human-machine interaction
illustrated on a set of well-known case studies in the HMI domain, and a
detailed overview of past, current and future developments of formal methods
in HCI. Unlike those previous works, this paper surveys all models of human
operators for the verification of human-machine systems, not just models for
formal verification, but also models for simulation and execution. The prior
works also surveyed broader set of application domains unlike this work which
is primarily driven by the need for a human-autonomy virtual engineering
platform as shown in Figure 1.

##  II Foundational Concepts

This section reviews some foundational concepts of human behavior including
perception, cognition, decision-making and actuation. Motivated by Boyd’s OODA
loop from his writing on combat operational process [2], the OODA loop
consists of four stages: observe, orient, decide and act. _Observe_ is the
ability of humans to perceive and sense the environment around them. In
Section II-A, some basic theories of human perception (primarily visual) are
surveyed. _Orient_ is the ability of humans to process the information coming
from their sensory sub-systems, understand it, and make predictions based on
such understanding. This ability is provided by the cognitive processes of the
human. In Section II-B, we discuss briefly the theories of human cognition.
_Decide_ is the ability of humans to create course of actions based on goals,
utility or payoff functions, and available information. Fundamental concepts
in human decision-making are surveyed in Section II-C. Finally, _act_ is the
execution of plans, which is briefly discussed in Section II-D.

###  II-A Perception

A fundamental framework for building models of human perception is Signal
Detection Theory (SDT) [5], which is is one of most successful quantitative
theories of human performance [6]. It is an experimental framework in which
the human participants are asked to detect the signal within a noisy input
stimulus. The participant’s reaction time and accuracy are recorded, and are
used to build a model of sensitivity and response bias.

In human perception modeling, one of the central questions that researchers
seek to answer is how efficiently can a human operator find a specific area of
information on a visual display, a task also known as _visual search_. A noisy
stimulus, in the context of visual search, can be the presence of items of
distractions on a display with the target item. Examples of using the SDT
framework for building models of human visual search include [7, 8], and
numerous other works which can be found in the survey paper [9].

A notable work in human visual attention is the feature integration theory of
Treisman & Gelade [10], which attempted to answer the question about the
serial and/or parallel characteristics of the visual process. Their model
hypothesizes that feature search is mostly parallel while other visual
processes are serial. In contrast, the work of Bundeson in [11] contains a
model with a strictly parallel architecture. The parallel argument can be
traced back to skepticism about distinguishing the serial processes from the
parallel process in works such as [12]. Some early theories on the mental
effort of human visual attention and processing can be found in [13] where the
performance is dependent on a single pool of undifferentiated resources. This
work later progressed into theory of multiple-resources [14] (MRT), where
attention and processing resources are divided into certain differentiated
pools.

###  II-B Cognition

A theory of cognition describes human cognitive processes such as reasoning,
problem solving, decision-making, language processing, memory, and learning.
The development of a theory of cognition is a multi-disciplinary effort that
spans linguistics, artificial intelligence, psychology, and sociological,
neurological and behavior sciences. A comprehensive review of cognition is
beyond the scope of this paper. Instead, we survey the efforts to unify and
codify cognitive principles into a common framework for building computational
models of human cognition, reasoning and learning. These common frameworks,
also referred to as cognitive architectures, are collections of structural and
mechanistic descriptions of “what human cognitive behaviors have in common"
[15]. Cognitive architecture models are the realization of the unified
theories of human cognition and reasoning in the form of computer programs
that simulate underlying cognitive processes of the human, and predict various
cognitive outcomes or phenomena. They are based on both fundamental theories
about the human cognitive process and assumptions about the domain being
modelled such as language acquisition, helicopter pilot training, expert
behaviors, or implicit learning. One of the earliest cognitive models was the
EPAM (Elementary Perceiver and Memorizer) [16] by Simon et al. It is a
quantitative model based on the verbal learning of nonsense syllables, which
predicts the rate of verbal learning as a function of parameters such as
familiarity, meaningfulness, and similarity. More recently, the trend has been
to unify the theories of the cognitive processes, and then formalize them as a
basis for a programming language environment which allows the end-users to
write programs that are executable models of the human mind.

###  II-C Decision Making

Models of human decision making range from game theory in economics [17],
where each agent minimizes or maximizes a utility function, to sub-optimal
descriptive models (behavioral economics) [18], where the model tries to
reproduce the heuristics of actual human decisions based on various human
idiosyncrasies such as bounded rationality [19] and over-confidence in their
knowledge [20]. Other works on informal heuristics of human decision making
include [21, 22, 23]. In a similar vein, the notion of satisficing decision-
making, which originated in Herbert Simon’s 1947 work on administrative theory
and refined over the years in subsequent works such as [24], relaxes the
notion of the maximization of utility to simplify decision making under large
uncertainty and poorly defined utility function [25]. In the satisficing
decision-making framework, the limited informational and computational
capacities of the human are taken into account. A decision is made if a simple
payoff function exceeds a certain threshold value, which captures the process
of making decisions of unknown optimality that are “good enough” for a given
problem.

From the field of psychology, the lens model from Brunswik’s 1952 work [26]
became an important conceptual framework for modeling human decision-making.
The main idea behind the lens model is that one can quantitatively capture a
human judgment of a criterion using a finite set of cues or observations
related to the criterion. Examples include a manager making a judgment on the
future success of a candidate (the criterion) based on the behavior that the
candidate exhibits during an interview (the cues), or a financial analyst
making a prediction on the future movements of a stock (the criterion) based
on current social media news (the cues). The typical lens model consists of
two halves. Each half is a multi-linear regression model. The right half
captures the relations between the cues and the human judgment. The left half
captures the relations between the cues and the actual outcome of the
criterion. A meta-survey of the lens model can be found in [27].

###  II-D Actuation

Actuation refers to the motor outputs of the human operator. The typical motor
outputs that are modeled in human factors research include simple tasks such
as pointing, dragging, clicking, gazing, steering, etc. Other forms of
actuation such as verbal or non-verbal body movements are not described here.
A fundamental model of actuation is the Hyman-Hick law [28, 29], which
hypothesized that the difficulty of a motor task is proportional to the
entropy of the situation. More commonly, the Hyman-Hick law is known in the
context of decision-making i.e. more choices equates to higher entropy which
means the person will take longer to make a decision.

While Hyman-Hick established an information-theoretic foundation for the
performance modeling of motor tasks, it did not become the dominant modeling
framework. Instead the most ubiquitous modeling framework in quantifying human
motor performance is Fitts’ law [30, 31], which relates the difficulty of a
task to the amount of information that needs to be transmitted over a
hypothetical communication channel of limited capacity. The time performance
of the motor task is linearly correlated with the amount of information
transmitted by the task. Consider the pointing task in which a person is
required to move a finger to a target on the screen. The signal for this task
is the distance $D$ to the target, and the noise is the width $W$ of the
target. A model capturing the difficulty of the task would be the entropy of
the task i.e. $\log{\frac{D}{W}}$. Fitt’s model has been generalized to other
tasks beyond finger pointing such as mouse, trackball, stylus, touchpad,
helmet-mounted sights, eye tracker and joy stick [32], and also generalized to
predict errors in motor tasks [33].

Beyond Fitt’s law, a more recent work by Accot et al. [34] extended the
informational-theoretic framework to cover complex motor tasks that are more
trajectory based. Examples of these motor tasks include steering, drawing
curves, navigating through nested menus, moving in a 3D world, which becomes
more relevant as interfaces move beyond the simple point and click paradigm.

##  III Hidden States and Failure Modes

This section introduces various hidden states or latent variables used in
models for predicting human performance in HMS. Many of these hidden states
such as workload, situational awareness, trust, vigilance, and boredom, are
understood qualitatively but are difficult to define precisely and to measure
directly. Despite their controversial status [35], they have proven to be
useful for creating engineering models for the design and V&V of HMS.

In addition to performance, the V&V process must guarantee safety of a HMS.
Traditionally, the human operator is not taken into account in safety analysis
except as a mitigation factor for the system hazards identified. However,
humans fail too. Taking humans into account in the hazard analysis phase of
the design process requires modeling their failure modes. For this reason, we
introduce models of human errors, and specifically mode confusion.

###  III-A Workload

Mental workload is extensively studied in human factors [36]. It stems from
the study of attention and information processing by cognitive psychologists
[37]. Mental workload is conceived to be a multi-dimensional construct of time
stress, mental effort and psychological stress [38, 39, 40] that is
independent of behavior and performance [41]. There is no commonly accepted
formal definition of workload, however generally speaking, workload is often
defined in terms of a relation between the mental resources required by a task
and the available mental resources that are supplied by the human. In [37], it
is noted that every human has a bounded set of resources available at any
given time. Early workload literature hypothesized that this pool of resources
was singular and undifferentiated [42]. The prevailing current theory of
workload is that the pool of resources is multi-dimensional i.e. that it is
divided into different channels of capacities [43, 44, 14]. The idea of
different channels of capacities of resources was introduced in works such as
[13] and eventually developed into what is known as the multiple resource
theory (MRT) [45]. In MRT, the human operator has separate resource blocks
that span multiple dimensions of input modalities, cognitive stages, and code
processing. In the modalities dimension, we find the visual, auditory, tactile
and olfactory blocks. In the stages dimension, we find the perception,
processing, and action blocks. Some empirical evidence providing the
separation between perception, processing and action resources can be found in
[46]. In the codes dimension, there are the symbolic (spatial) and the
linguistic (verbal) blocks. The codes dimension is based on the hemispheric
laterality framework where some tasks are exclusively executed by a certain
hemisphere of the brain (the left brain versus right brain paradigm). In MRT,
the degradation of the human performance is simply the result of overloading
in any of the individual resource blocks due to the performance of one or more
tasks. Using the MRT model, the phenomenon of cross-task interference can be
measured by quantifying the amount and the type of resources taken up by each
of the tasks.

Other workload theories in the literature can be interpreted as a special
instance of the multiple resource theory either by using a hemispheric
dimension in [47, 48], by expanding one dimension into other sub-dimensions in
[49], or by restricting to only one dimension in [50]. The response selection
bottleneck theory of Pashler [50] is an example of multiple resource theory
that captures concurrent task interference only within the stages dimension.
In Pashler’s model, the interference between the two tasks is total, meaning
that the response selection portion (processing stage) of the task acts like a
semaphore which uses all of the available resources of the human operator.
Underlying the bottleneck theory is the theory of psychological refractory
period (PRP) [51] which establishes that the human operator’s ability to
respond to external stimuli is completely degraded during a certain period
right after it has received an earlier stimulus. The PRP phenomenon is
captured in the perceptual modality within the EPIC cognitive architecture
[52].

Workload is difficult to measure as it is context and operator-dependent.
Disassociations can occur frequently between the different measures of
workload [41]. Workload varies based on many factors such as individual’s
capabilities, environment factors, and the difficulty, type, timing, and
criticality of the task [53]. There are 3 predominant basis to measure
workload: performance, subjective evaluation ratings, and psycho-physiological
measurements. Inferring workload using task performance measurements can be
problematic. There is empirical evidence that low workload leads to degraded
performance [54]. The latter can be caused by, for example, the induced
boredom in the human operator, which has an effect on human vigilance [55]. It
has been noted that more often than not, task performance fails to reflect the
resource re-allocation prompted by the changes in the task demands [39]. For
example, the human operator frequently adjusts its effort in response to more
challenging tasks. Workload measures can disassociate from performance
measures [41] for both simple or challenging tasks. Nonetheless performance-
based measures of either primary or secondary tasks is a widely-used approach
to evaluate workload and human-machine system performance in various contexts
[56, 57].

###  III-B Situational Awareness

Situation awareness (SA) is defined by Endsley in [58] as “knowing what is
going on around you” with an inherent notion of knowing what is important.
Many other definitions of SA have been developed either in the domain of
aviation or more general applications. A good survey of SA definitions
relating to aircraft piloting can be found in [59].

Endsley gave a detailed descriptive model of SA in [60] as having a
hierarchical structure, with the first level being perception, the second
level being comprehension, and the third level being projection. The last
level captures the capability of the human operator to not only being able to
comprehend the current state of the situation, but also to understand what is
going to happen in the future. In the Endsley model, SA is a separate stage
from decision making because it represents the construction of the human
operator’s internal model of the external world. Any decisions that the
operator made in constructing this internal world has no impact on the
external world. Moreover it has been observed that human operators can make
poor decisions even during a state of excellent situational awareness.

###  III-C Vigilance, Boredom, and Complacency

The notion of complacency is mentioned frequently in the aviation human
factors literature [61] and the term has long been absorbed into the
vernacular of aviation accident reports [62, 63] as a causal factor. In a
survey of leading airline captains [64], more than half thought that
complacency was the leading cause of aviation accidents. The notion is
considered by some as controversial. It is criticized, along with other
concepts such as SA, mental workload, and trust as “folk” models in [35] with
little underlying scientific basis and more common sense appeal. A counter-
argument is given in [65] supporting these notions with an extensive data-base
of empirical evidences, computational models and psychological foundations
supporting SA, mental workload and trust.

Wiener in [64] discussed complacency as a low level of suspicion but suggested
more empirical research to understand any underlying mechanisms behind
complacency. In [66], complacency is a term used to explain the higher rate of
mis-detections of automation failure when the reliability of automation is
increased. While there is no consensus on the exact definition of complacency,
it is suggested in [67] that a working definition could be derived from the
features of complacency common to both aviation accidental analyses and human
performance studies. This set of features include human monitoring of
automation, a sub-optimal frequency of monitoring of the automation [68], and
finally observable degradation in system performance due to the sub-optimal
monitoring. A conceptual model of complacency is given [67]. In this model,
complacency is a dynamic variable that varies overtime through interactions
with the automation, and affects the attention allocation of the operator,
which in turns may or may not lead to errors in the operation of machines.

Vigilance can be interpreted as the lack of complacency [66]. The notion of
vigilance is usually defined in the human factors literature as the ability of
the human operator to focus attention on a signal source for extended period
of time while remaining alert to a particular signal [69]. The study of
vigilance started with Mackworth’s work in World War 2 to understand why sonar
operators miss certain weak signals indicating the presence of submarines at
the end of their watch. A review of recent research on vigilance in [70]
shows, through various subjective reports and more objective physiological
measure of blood flow within the brain, that maintaining vigilance require
high workload, and that a decrease in vigilance over extended period of time
can be explained by the attentional resource theory of MRT.

As discussed in the survey in [71], boredom is closely related to vigilance,
complacency and attention management. The prevailing view is that boredom is
caused by the monotony or repetitiveness of tasks that require constant
attention [72, 73]. Alternatively, a more recent view is that low task loading
such as passive monitoring of autonomous systems [71] also contributes to
boredom. Given the current trend of increasing autonomy in aviation, boredom
leading to complacency [74] could result in increasing number of problems.

###  III-D Trust

Trust is often defined in the various human sciences as some expectation by
the human of certain outcome behavior. As stated by the Harvard sociologist
Bernard Barber in [75], it is the “expectation of technically competent role
performance.” Some of the earliest works on human trust in the automation
domain can be found in [76, 77] where trust was raised as a factor in the
context of modeling the supervisory control of computer or automation. In
these early works, the main hypothesis is that trust has an impact on the
supervisor’s intervention behavior, and the quality of the automation was
raised as a factor in affecting trust. Some early conceptual models of human
trust in automation performing continuous process control include [78, 79, 80]
which related the various factors including the use and mis-use of automation,
the trust of the operator in the automation, and the competence of the
automation. The authors in [80] validated their conceptual model with two
experiments, one qualitative and the other quantitative, involving an
automatic process control [81]. The experiments showed that trust can be
eroded by temporary automation errors that have no consequence on the long
term operation of the system, and it also showed that trust is not a binary
variable but rather that there are multiple and possibly continuous levels of
trust. The work in [79] provided a mathematical model of how trust and
confidence relate to the performance of the human-machine system. A
contextually focused approach was taken in [82] which produced a relatively
early computational model of trust. In [82], trust is qualitatively a
“context-specific” argument against the performance of the system, and
quantitatively a probability distribution of the correctness of the system
actions given the system and the context or situation. In this framework, the
problem of the acceptance of the output of decision support tools is not due
to some steady state notion of under or over-trust but rather to a context-
specific, transient notion of “inappropriate trust” in which there is a
failure by the human operator to understand the conditions leading to either
good or bad performance of the decision support tools.

###  III-E Failure Modes: Human Errors and Mode Confusion

The main approach to modeling human errors has been to use the phenotypical
types as described by Hollnagel in [83]. The increase in reliability of
aircraft systems has in turn highlighted cockpit crew error as a major cause
of aviation incidents in recent years. A comprehensive framework that
discusses human errors in aviation can be found in [84]. The taxonomy
framework, known as Human Factors Analysis and Classification System (HFACS),
has its theoretical groundings in Reason’s swiss-cheese model of human errors
[85], and groups human errors in aviation into 19 causal categories ranging
from crew resource management errors [86] to individual errors in decision-
making, perception and the execution of skill-based flying. Navigation errors
are defined in [87] as when the aircraft has moved into an uncleared taxiway
or when the aircraft has deviated from the centerline in a cleared taxiway. As
indicated by its definition, navigation errors occur only during surface or
runway operations. Cockpit task management (CTM) errors occur when pilots
initiate, monitor, prioritize and terminate concurrent cockpit tasks. The
increase in automation of aircraft systems has resulted in a corresponding
increase in CTM errors as a factor in aviation incidents. Empirical studies in
[88] show that CTM errors occurred in nearly 23% of aviation incidents
surveyed in the work.

Mode confusion is the result of discrepancies between the human operator’s
mental model of the machine, and the actual state of the machine. Due to the
increasing complexity of aviation systems, mode confusion has been identified
as a contributing factor to many recent aviation incidents [89]. Mode
confusion was rigorously defined in [90] using a failure refinement (or lack
of) relation between two processes. One process contains the safety-relevant
system behavior as sensed by the human operator, and the latter process
contains the operator’s mental model of the safety-relevant system behavior.
Leveson et al. in [91] discusses some of the common design flaws which can
lead to mode confusion such as interface interpretation error (the user does
not interpret the interface purpose correctly), indirect mode changes
(automation mode changes that occur without explicit command from the user),
inconsistent behaviors (automation exhibits the same behavior in many modes
except for one or few), and lack of appropriate feedback (automation does not
provide the right visual/aural indications to the user that the mode has
changed).

##  IV Formal Models

This section samples humans models used in the _formal verification_ of human-
machine systems.

In formal verification, models of human, machine and the properties of
interest (safety and/or performance) to be verified are captured using formal
language(s) with unambiguous mathematical meaning. The human-machine system is
verified when a proof is generated that shows that the system satisfies the
properties of interest. This proof is typically either automatically generated
using model-checking [92], or semi-automatically using a proof assistant [93].

###  IV-A Formal Model of Tasks

We survey some efforts to formalize task and cognitive models of human
operators. A more detailed review of various formal task and cognitive models
can be found in this earlier survey paper [94]. Formal models of human
operators have been developed in the past using general languages such as
process algebra [95], Petri-Nets [96], and more domain specific ones such as
task analytic or cognitive modeling languages. This review focuses on the
latter two as process algebra and Petri-Nets are already formal
representations with well defined semantics and a variety of analysis tools
already available to users, and the main issue is, therefore, the encoding
process to represent a human model.

Task analytic models are hierarchical representations of the observable set of
human behaviors. In a task model, a high-level activity is decomposed into a
set of composite actions which are further decomposed into a set of atomic
actions. Some task analytic modeling languages are ConcurTaskTrees (CTT) [97],
Operator Function Model (OFM)[98], Enhanced Operator Function Models (EOFM)
[99], and User Action Notation (UAN) [100]. Formal task analytic models can be
encoded in a task modeling language, and then translated into a model checking
or theorem proving representation for analysis and verification (see [101,
102, 103, 104]). They can also be directly encoded in the formal language.
Task model analyses in general are more limited by scalability issues than
interface analyses since they cover the system beyond the interface.
Nevertheless they have been extended to analyses with a team of operators or
multiple operators (see [105, 106]) and errors [107]

###  IV-B Formal Model of Cognition

Lindsay and Connelly et al. in [108] applied model checking on a human
operator model expressed in the cognitive architecture Operator Choice Model
(OCM), and the approach was then applied in [109] to study erroneous behaviors
of human air traffic controllers for various ATC tasks. OCM is not a generic
cognitive architecture as it is specialized for ATC tasks. Other works on more
generic cognitive models such as Programmable User Models (PUM) include
Blandford, Curzon, Butterworth et al. in [110, 111, 112, 113]. The
verification in [111] was done using a theorem proving approach while [113]
used model-checking. One advantage that a cognitive model has over a task
analytic model is that it can capture the organic underlying reasons for human
errors rather than requiring researchers to introduce them explicitly into the
model. The main drawback of cognitive models is that they are more complex
hence less tractable by formal verification techniques. The work in [114] is
an example of assessment of human errors in the context of ATM. The work by
Masci et al. in [115] uses the theorem-proving language PVS [116] to model a
distributed cognitive model describing the information flow among multiple
human operators. Distributed cognition [117] is a conceptual framework in
which cognition is a property of the whole system i.e. not just confined to
the human minds. Additionally, a recent work in [118] approached the problem
by translating an existing cognitive model into a formal language
representation. The cognitive model, a SOAR model of air traffic contingency
procedures performed by a human and automation team, was translated into a
hybrid input-output automaton, which was then used to formally verify safety
properties as the autonomy level of the system was increased.

###  IV-C Formal Models of Workload

Formal models of workload is a relatively unexplored area. In [119], the
authors argued that one limitation of existing workload models is their level
of resolution being too detailed and thus requiring modeling efforts that are
impractically time-consuming. To address this limitation, they created an
abstraction of a UAS-human teaming scenario with all of its actors modelled by
finite-state machines augmented with workload metrics. Behavioral execution
traces of the FSM model result in traces of workload metrics which can be
monitored for violation of specification. Moore et. al however did not present
any formal verification results. A more recent work [120] presented a novel
approach which combined model-checking and simulation for the analysis of task
loads and resource conflicts in air traffic control scenarios. In this work, a
trace of an air traffic simulation model for a particular scenario and time
window is translated into a timed-automata model, which is used to model-check
the entire “neighborhood” around the particular scenario for any violation of
key properties. The counter-examples obtained by the model-checker are then
fed back to the simulator for further analysis using higher fidelity models.

###  IV-D Formal Model of Failure Modes

Mode confusion have been analyzed formally using either model-checking and/or
theorem proving (see [121, 122, 123]). In all of those works, the human
operator was not modelled modulo the human inputs to the machine. In [121] for
example, model-checking and theorem proving were used to explore all the
unexpected inputs that can trigger a particular flight guidance mode. Other
approaches towards formal analysis of mode confusion include modeling what the
operator thinks is the state of the machine (also referred to as the mental
model) [124, 125], or how the operator accomplishes goals using the machine
(also referred to as knowledge model) [126]. Crow et al. in [127] proposed
that mental models should be constructed from questionnaires to be
incrementally refined and verified until the smallest safe mental model is
found. However, extracting an accurate mental model from a human operator
remains a challenge. In [128], the automation interface design tool ADEPT was
used for the analysis of mode confusion. Based on the mental model paradigm,
the system and mental model are captured in ADEPT using an enriched labelled
transition system called HMILTS.

In the context of formal verification, one of the main approach to classifying
and modeling human errors has been the binary phenotypes as described by
Hollnagel in [83]. Several works [129, 130, 131] have incorporated Hollnagel’s
phenotypes of error into their task models and used model-checking to
determine whether the errors would lead to any violation of the
specifications.

A more recent taxonomy of human errors developed to be more aligned with task
analytic modeling and analysis techniques has been proposed in [132]. This
taxonomy was first applied in [133] and then in [134]. In the latter work,
reliability analysis and probabilistic model-checking were used to verify
temporal-stochastic specifications such as the probability of an eventual
failure being reached is less than some time bound. This supports the
alternative view of human errors as probabilistic distributions of behavioral
outputs under cognitive, motor and perceptual constraints.

###  IV-E Formal Model of Knowledge

The epistemic approach [135] uses modal logic to capture and reason about the
belief and knowledge of multi-agent systems. While epistemic modal logic has
been studied for the past several decades [136], there appears to be little
work which uses this framework to describe and reason about human behaviors in
general. One possible reason is the lack of modeling tools that are intuitive
to the domain expert. This could be due to the lack of a grounded semantics
for the systems under analysis which in our case is the human operator. The
interpreted system [135] model has a well-known grounded semantics that has
been used to model knowledge, belief and communications of computing systems.

Another possible reason is the dearth of efficient verification tools. Though
recent model-checking literature [137, 138, 139] have tackled the problem of
verifying various language fragments with temporal and knowledge modalities,
there are only a few modeling and verification tools that support epistemic
and temporal modalities. One such tool is the MCMAS, described in [140, 141],
which was developed for the verification of multi-agent interpreted systems.

Perhaps another weakness of the epistemic approach is the problem of logical
omniscience: an agent knows all the consequences of a set of logical
assertions. Logical omniscience does not capture human characteristics such as
bounded rationality, bounded reasoning and introspective forgetting. Various
modifications to the epistemic approach have been proposed to address logical
omniscience such as impossible possible worlds [142], algorithmic knowledge
[143], and non-classical propositional logic [144]. Other research works such
as the one in [145] have proposed ways of enhancing the expressiveness of
epistemic logic in order to succinctly capture introspective forgetting.

Relative to task and workload models, the literature on modeling of knowledge
and belief of human operators is very limited. The work in [146] extended CTLK
(a temporal-epistemic first-order logic) with a notion of degree of belief,
and introduced a model-checking algorithm for such extended logic. The authors
applied this extension to the Air France 447 (AF447) incident and duplicated
the NTSB conclusion that right before the crash, the pilots did not believe
any of the signals coming out of the cockpit display were true. The same case
study was used to illustrate agent safety logic (ASL) in [147], a modal logic
formalized in Coq [148] with both epistemic and doxastic (belief) modalities
combined with a safety logic based on the flight manual. ASL was used to
illustrate the increasingly common phenomenon in aviation in which the pilot
neither knows the state of the aircraft nor knows that he or she does not know
the state of the aircraft.

###  IV-F Comparative summary

Table II lists the models we have surveyed in this section. Each model is
classified in terms of six key attributes that we believe are important for
the formal verification of HMS. _Focus_ is the primary aspect of the human
considered by the model. _Formal verification_ is the technique used to prove
properties about the model, and can be either model-checking or theorem
proving. By “model-checking” we mean any tool that performs symbolic or
explicit state-space exploration, and that is typically fully automatic. By
“theorem proving”, we meant a proof assistant tool such as PVS or Coq which is
interactive. _Timing_ indicates whether the cited work has demonstrated the
ability to verify non-trivial properties that involve time (either discrete or
continuous). The use of temporal logic alone would not be considered as
evidence that the model can handle properties about time. The same rationale
applies to _Probabilistic_ and _Epistemic_. The former indicates the ability
to handle systematic uncertainty and answer queries about the probability of
certain events. The latter indicates the ability to formally reason about the
belief of the human. Finally, the _Tool_ column indicates whether the work has
produced an integrated tool-chain with a frontend modeling environment that is
connected to backend solver(s) for verification.

Table II shows a general lack of support for uncertainty, both systematic and
epistemic, which is expected given the inherent complexity of the verification
problem for uncertain systems. Furthermore, there seem to be a lack of
interest in the development of integrated tools bridging the gap between
models and formal verification engines.

TABLE II: Summary of surveyed formal verification models Model | Focus | Formal Verification | Timing | Probabilistic | Epistemic | Tool
---|---|---|---|---|---|---
Multiple [99, 103] | Task | Model checking | No | No | No | No
Multiple [101, 102, 104] | Task | Theorem proving | No | No | No | No
Butterworth et al. [111] | Cognition | Theorem proving | Yes | No | No | No
Rukvsenas et al. [113] | Cognition | Model checking | Yes | No | No | No
Musci et al. [115] | Distributed Cognition | Theorem proving | No | No | Yes | No
Multiple [124, 125] | Mode confusion | Model checking | No | No | No | No
Houser et al. [120] | Workload | Model checking | Yes | No | No | No
Moore et al. [119] | Workload | No | Yes | No | No | No
Bolton, Zheng et al. [134] | Task + Error | Model checking | Yes | Yes | No | No
Multiple [129, 130, 131, 133] | Task + Error | Model-checking | No | No | No | No
Primero et al. [146] | Beliefs | Model-checking | No | No | Yes | No
Ahrenbach et al. [147] | Beliefs | Theorem proving | No | No | Yes | No

##  V Simulation Models

This section presents a survey of the simulation (or computational) models. By
simulation, we also mean models that are compiled and then executed.
Simulation models tend to contain more details than formal models, but
verification using simulations is non-exhaustive in the sense that for most
cases, it is not possible to simulate all possible inputs.

###  V-A Models of Visual Processes

Some of the more recent works in building visual attention models for
simulation include a cognitive architectural model with eye-tracking data in
[149], a salience model [150] for computerized scene analysis, and a Markov
model in [151]. The salience model [150] led to many further works in robotics
on duplicating the human visual capability. The model is based on a
biologically-plausible architecture by Koch and Ullman [152]. It assumes the
existence of a master salience map [153] in the posterior parietal cortex of
primates that is influenced by top-down factors such goals and knowledge. This
salience map is also influenced by a topographical map computed in a bottom-up
parallel process from feature maps (color, intensity, orientation, etc.)
generated from the input scenery. The regions on the salience map with the
highest values correspond to a more rapid or accurate response from the human
operator. A recent significant advancement within the salience framework is a
fast computational model based only on the log spectrum of the input image
[154].

Another important question that is addressed by perception modeling is _visual
attention allocation_ , namely how much attention from the human operator a
given area of the display captures relative to other areas. An analytic model
for computing attention allocation is the SEEV (Salience, Effort, Expectancy,
and Value) model [155]. This model was developed for aviation applications,
such as pilots in the flight deck [156], and has been extended to models of
visual attention of drivers [157]. The model is a simple function of four
different variables: salience (the likelihood that the visual event will
attract attention), effort (the amount of effort required to re-allocate
attention to the event), expectancy (the bandwidth and rate of information
flow generated by the event), and value (a measure of the cost of not
processing the event [158]). The output of the function is the probability
that a given area of the interface display will attract the operator’s
attention.

Most recent developments in computer vision have been based on very large
convolutional neural networks (CNN) [159, 160, 161] trained on very large
datasets [162] for tasks such as image classification and detection. The
effective use of a black box model such as a CNN for the purpose of verifying
human performance remains an open question.

###  V-B Models of Cognition

For cognition, sophisticated simulation models such as cognitive architectures
have been applied in a wide variety of domains ranging from education [163] to
aviation (see NASA and AFRL studies in [164, 165]). Some examples of state-of-
art cognitive architectures include ACT-R [166], SOAR [167, 168], CHREST
(Chunk Hierarchy and Retrieval Structure) [169], ICARUS [170], and MIDAS
[171]. The shared features of these cognitive architectures are:

  1. 1.

A collection of underlying knowledge about the human intelligence such as how
short and long-term memories are formed and retrieved, and how the information
from memory gets processed.

  2. 2.

The production system representation which is an executable program with a set
of rules governing the behavior of an underlying phenomenon that it is
describing.

  3. 3.

The problem space approach, which includes a desired final state (also called
goal), the initial state, a set of the operators from a problem space that
when applied to a state lead to another state, and the search strategy over
the problem space.

Some cognitive architectures are specialized for certain applications. The
EPIC architecture of Meyer and Kieras [52], for example, is especially suited
for modeling multi-modal and multi-task performance. Another example is the
GOMS (Goals, Operators, Methods, and Selection) architecture [172], a simple
cognitive architecture used to make qualitative and quantitative predictions
for normative or repetitive cognitive tasks in the domain of human-computer
interaction. In the context of aviation, the GOMS framework has been used in
the analysis of an advanced automated cockpit [173], and the ACT-R
architecture has been used in modeling the differences in skill acquisition of
an ATC task [174]. Cognitive architectures have also incorporated other
aspects of the human operator including, but not limited to, perception,
sensing, and actuation [175]. Using a unified cognitive architecture such as
ACT-R, allows for developing a computational models of a human operator
executing a task in a particular domain.

###  V-C Models of Decision Making Processes

Mathematical representations of the lens model was developed in the works of
Hammond and Hursch [176], and has been applied to the study of air traffic
control systems such as the work in [177]. In this work, the authors quantify
the differences between the decisions made by a human air traffic controller
against the decisions of the automated air-collision alert algorithm. The
mathematical model has the following structure: the human judgment is assumed
to be a probabilistic affine function of the cues, the environmental criterion
under judgment is assumed to be another probabilistic affine function of the
cues, and the measure of the accuracy of the human judgment is a nonlinear
function of the correlation of the two function outputs, the predictability of
the two functions, and the correlation between the errors of the two function
outputs.

Another approach involves building expert systems, which are computer programs
that mimic expert decision-making. In an expert system, the decision-making
process of the human is captured by an inference process, driven by if-then-
else rules that use known facts from a knowledge database. In domains such as
aviation, expert systems [178] have been created to automate some of the
functionality that were previously allocated to the human. In that sense, an
expert system is a functional model of human decision-making.

Simulation models of human decision-making have also utilized formalisms
ranging from stochastic processes to continuous dynamical systems. One such
modeling framework is the decision field theory (DFT) [179] which attempts to
capture the dynamics of the human cognitive process in decision-making using a
diffusion process, and has been used to predict response time and course of
action under timing constraints and uncertainties. In the context of air
traffic control (ATC) in the National Airspace System (NAS), models ranging
from a Partially Observable Markov-Decision Process (POMDP) in [180], to a
Dynamic Bayesian Network (DBN) in [181] have been used. Furthermore, there are
game-theoretic models such as the one in [182], and dynamical system models of
human decision making such as the dead-reckoning navigational filter model
used in [183] or the Markov chain of Kalman filters used in [184]. Finally, a
quantum dynamics model of human decision making (i.e. a model that describes
the evolution of probabilistic amplitudes) was presented in [185] and compared
with a Markovian model.

###  V-D Models of Tasks

Task analysis, and its specialized sub-field of cognitive task analysis (CTA)
[186] is a large collection of methods and tools for extracting expert
knowledge, thought processes, and goals in the performance of tasks. In
another words, it is an approach to describe the physical and cognitive tasks
to accomplish an activity. CTA is done for both observed behavior and latent
cognitive functions. It has been applied widely in the aviation domain [187,
188] as a knowledge capturing mechanism. With increased frequency, CTA is used
by airlines and the air traffic control community for the design of automation
and training on the flight deck, operations, and the flight control tower. For
example, in [189], the results of a CTA are used as inputs for modeling human
operator performance in approach, landing, ATC, and ground operations of a
single piloted aircraft. Task analysis are typically performed to capture
expert knowledge such as task definitions and decomposition of missions. Task
definitions and decomposition are important steps to build task models for
tools such as IMPRINT or other discrete-event simulators so that performance,
typically workload, can be assessed for the scenario or application at hand.

In [107], a task hierarchical notation called HAMSTER augments the typical
task hierarchy modeling formalism with information about system failures and
human errors to analyze their effects on operator performance.

###  V-E Models of Workload

There are numerous mental workload modeling methodology and tools, based on
the multiple resources theory (MRT), for the simulation and prediction of
operator performance. They are especially useful for cases where it is not
feasible to perform experiments on the actual system, environment and
operators. The task analysis workload (TAWL) framework [190] and the TAWL
operator simulation system (TOSS) was an early methodology developed for the
prediction of operator workload. In the methodology, mission segments are
decomposed into individual tasks, that are then modeled and simulated. This
methodology bears resemblance to the task network modeling paradigm in the
operator workload prediction tool IMPRINT [191]. Cognitive architectures such
as the MIDAS performance tool [171] and ACT-R have also incorporated workload
modeling methodology based on the MRT.

Various computational models of multiple resource theory can be found in [192,
193, 194] where [193] is a simpler version of the model in [192] and applied
to the prediction of driving performance and interference in [194]. These
computational models can be distinguished from tools such as IMPRINT in that
they can be used to predict more than just resource demand, but also task
interference and re-allocation of resources. Unlike most of the mental
workload tools, MRT computational models can capture both cases when residual
capacities exist in the human operator as well as when the operator is
overloaded. The principle of multiple-resources has been used in various
applications such as the development of cognitive architecture models for
predicting workload [195], analysis of new cockpit display designs [196], and
air traffic safety management [197].

It was noted in [198] that different performance metrics across different
tasks make standardization of a performance-based workload measure difficult
across domains. Subjective evaluation techniques such as SWAT [40] or the
NASA-TLX (task load index) [199] are methods that rely on self-reported
ratings from operators, and/or observers. This is the most common technique
used for the measurement of workload. There are both one-dimensional and
multi-dimensional workload rating scales in the literature. The latter
typically aggregates the individual ratings into a single final workload value
using either pair-wise weightings [199] or conjoint analysis [40]. The multi-
dimensional scaled ratings are based on the assumption that the operator can
evaluate the individual components of the workload better than the overall
workload. Finally, the psycho-physiological techniques [200, 201, 202, 203,
204] attempt to quantify workload by interpreting the measures of physical and
neurological cues such as heart rate, EEG output, eye movements, pupil
response, respiration rate, blood pressure, and sinus abnormalities.

###  V-F Models of Situational Awareness

An early computational model of SA can be found in the work by Shively et al.
[205]. This model is build within the MIDAS environment, and became the
foundations for the more recent computational model A-SA [206]. The A-SA
consists of a low-level attention module coupled with a high-level belief
module. The attention and belief modules are based on existing models of
cognition and perception. For example, the attention module in A-SA is
borrowed from Bundesen’s 1990 work on the theory of visual attention [11]
which has similarities with the more advanced SEEV model introduced earlier.
The output of the model is a SA decay curve, in which the rate of decay is a
function of the distance between the evidences produced by the visual module
and the operator’s current internal model of the world. The A-SA model has
been mostly applied to applications in aviation such as pilot errors [207].

###  V-G Models of Trust

In [208, 209, 210] the relations between the many variables in a human-machine
system such as workload, difficulty of the task, system failure types,
automation reliability, and interface display, are related to the notion of
trust in the automation. A dynamical model was discussed in the survey paper
[211] where trust is dependent on a dynamical interaction between the
operator, the interface, the automation, and the context. A closed-loop model
of trust versus reliance was provided in which the interaction with the
automation influences trust which in turn affects the interaction with the
automation. Although there are many conceptual models of trust, only few
computational models exist in the literature. In [212], a stochastic process
model of decision-making in the context of human supervisory control, i.e. a
binary decision process between manual control and automation control, was
used to capture trust in a dynamic setting. This model, which extends decision
field theory to take into account prior decisions in a sequential decisions
process, replicates several empirical nonlinear relations between trust, self-
confidence and reliance. In [213], a real-time multi-modal model of trust was
produced based on structured equation modeling (SEM) [214] which is a
collection of statistical modeling and inference techniques that has had a
long history of usage in the social sciences [215].

###  V-H Integrated Modeling and Simulation Environments

A recent trend in human modeling research is to focus on the integration of
theories, models, and tools together into a complete human performance
modeling environment. Cognitive architectures such as SOAR and ACT-R are some
of the most popular examples of integrated modeling environments. Another
popular approach is based on a task network model where nodes (tasks) are
events with triggering conditions, side effects during and post-execution,
workload values, and probability of failures, and connections are transitions
between the tasks. These approach is general and can readily accept many
theories, models and data from the human operator modeling literature.
Workload assessment is done by running Monte-Carlo simulations on the task
network model using a discrete-event simulator. The tool IMPRINT [216] and its
early precursor SAINT [217] are some examples of discrete-event modeling
environment which have been specialized for assessing workload.

Recent integration efforts connect distinct modeling and simulation
environments together to handle more complex system-of-systems. An argument
for this approach is made in the introduction of [218]. As the system being
modeled becomes more complex, one modeling or simulation paradigm may not
cover all the possible domains in the system. Extending one paradigm to cover
the new domains may not be possible since its capability might be stretched
beyond those for which it is a natural fit. The approach to address this
problem is the integration of other environments that are already well-suited
for those new domains. An example of such effort is the IMPRINT/ACT-R
integration done in [219] which was used to model and simulate an approach and
landing problem provided by NASA. IMPRINT be naturally used for modeling all
sequences of tasks at hand, while ACT-R is a natural environment for
predicting human performance for each task. Another example is the composite
cognitive architecture QN-MHRP from [220] which connects a queuing network
model with a cognitive architecture in order to study human performance on
concurrent activities. Queuing networks are well-suited for modeling parallel
activities, while cognitive architectures are well-suited for predicting a
person’s action on a specific task.

Other more specialized integrated environments include the MIDAS tool by NASA
Ames [221], which is used in the design and analysis of cockpits and ATC
interfaces. The distributed operator model architecture (D-OMAR), which is a
multi-tasking extension of the event-based modeling architecture OMAR [222],
has been used for modeling pilots in various studies in aviation, one of which
is the NASA human performance modeling study reported in [223]. This study was
part of a multi-year effort [224], which detailed the modeling challenges and
solutions of five teams, each using a different human performance simulation
and modeling environment (ACT-R, ACT-R/IMPRINT, Air MIDAS, D-OMAR and A-SA),
to model and predict pilot performance and/or errors in two different
contexts: instrumented approach and landing, and taxiway operations. WMC or
Work Models that Compute [225, 226] is another integrated simulation framework
that has been used to study human performance in aviation [227]. WMC allows
the modeling of both the human and autonomous agents. The hybrid timing of its
simulation engine enables simulation of both continuous-time dynamical systems
and event-driven agents.

###  V-I Applications to Human-Aviation Systems

An early study of single-pilot operations in the context of evaluating new
advanced cockpit and control technologies for military helicopters can be
found in [228]. In this study, test pilots were used in experimental
simulations, and several subjective ratings scales including SWAT were used to
evaluate cockpit workload. It was found that despite the advances in the
cockpit, single-pilot operations increased workload. A model-based approach
was taken in [189] to evaluate single-pilot commercial operations, where a
two-pilots model built using the D-OMAR architecture was used as the baseline
for evaluating performance in the single-pilot case and prior cognitive task
analysis of approach, landing, and taxiing in [187] was used as insight for
the human performance models. It has been speculated in [229] that single-
pilot commercial aircraft can be designed using mostly existing technology and
available human factors models by re-designing the flight deck to re-allocate
some pilot functionality to automation and/or ground control.

Navigation errors have been modeled in D-OMAR [230] and ACT-R [231]. In the
former, navigation errors are captured in the model as the result of an
unconscious winner-take-all selection of the wrong “intention-to-act”, where
each “intention-to-act” is some pre-generated cognitive plan to be executed.
In the latter, the errors are revealed as the result of complex interactions
between the cognitive model of the pilot, co-pilot, air traffic controller,
and the model of the airport environment.

While experimental studies about single-pilot operations (SPO) in aircraft
goes back decades [228], there are only a few works in the literature that
have attempted the quantitative modeling and prediction of pilot performance
in a single-pilot cockpit. In both [232] and [233], a task analysis approach
was taken. In [233], task analysis of single-pilot concept of operations
architectures was performed. The scenarios modeled in this work were related
to the approach and landing portion of a flight into Denver airport. Task
models were visualized in the environment Mirco Saint Sharp. Performance
measures based on task counts and workload were compared against a baseline
scenario of current day crew complement. In [232], the modeling and simulation
framework Pilot-Autonomy Workload Simulation (PAWS) measured the utilization
of tasks, which has been applied in a prior work [234] to approximately
measure a pilot’s workload. A custom discrete-event simulator was built to
simulate the completions of tasks of various agents over the course of an
entire flight from take-off to landing. The framework enabled a flexible
configuration of different operational architectures, contingencies in
scenarios, and degree of autonomy of the cockpit.

The MDP framework was used in [235] to model the interactions between a human
operator and a UAV for the automatic synthesis of controllers. The human
operator was modelled using a DTMC, and the UAV as MDP. The two systems in
closed-loop form a product MDP, which is then processed by a MDP synthesis
algorithm to yield a controller for the UAV.

Recent works in [236, 237] have also modelled human behaviors using the HMM
approach. In [236], a HMM was used to model the human supervisory control
(HSC) of unmanned vehicles and then used for predicting the future actions of
the operator. In [237] the modeling of HSC is extended using a hidden semi-
Markov model in order to capture the timing of the transitions between the
states which is important when the operational tempo of the HSC needs to be
taken into account.

###  V-J Comparative summary

Table III lists the models we have surveyed in this section. The attributes we
have used to classify simulation models are similar to the ones in Section
IV-F, with the following differences. _Formalism_ refers to the structure of
the computational model used in simulation. _Stochastic_ indicates whether the
model can accommodate uncertainties in the inputs, outputs, and states of the
system, and whether simulation supports them. Similarly, _Epistemic_ refers to
the ability to model and simulate knowledge and beliefs. Finally, the _Tool_
column indicates whether there is an integrated tool-chain with a frontend
modeling environment that is connected to compilation, execution and
simulation back-ends.

We observe a general good support for time and systematic uncertainty. This is
expected given that simulation models often rely on discrete event simulation
engines, that probabilistic events can be handled using random number
generators, and that uncertainty quantification can therefore be done using
Monte-Carlo methods. However, handling more complex epistemic properties seems
to be out of reach. We also observe a pretty good availability of tools which
are typically easier to build than in the case of formal verification.

TABLE III: Summary of surveyed simulation models Model |  Focus | Formalism | Timing | Stochastic | Epistemic | Tool
---|---|---|---|---|---|---
Salience [150] |  Visual Attention | Neural Network | Yes | No | No | Yes
SEEV [155, 238] |  Visual Attention | Analytic | Yes | No | No | No
CNNs [159] |  Vision | Neural Network | Yes | No | No | Yes
ACT-R, SOAR, CHREST, ICARUS |  General Purpose | Cognitive Arch. | Yes | Yes | No | Yes
EPIC, GOMS |  Tasks | Cognitive Arch. | Yes | ? | No | Yes
LENS [177] |  Decision | Multi-linear regression | No | No | No |
Multiple [180, 181] |  Decision | Stochastic process | Yes | Yes | No | No
Tomlin et al. [182] |  Decision | Game-Theoretic | Yes | No | No | No
Multiple [183, 184] |  Decision | Dynamical Systems | Yes | No | No | No
Busemeyer [185] |  Decision | Quantum Dynamics | Yes | Yes | No | No
Shively et al. [205] |  SA | MIDAS | Yes | No | No | No
A-SA [206, 207] |  SA | Analytic | Yes | No | No | No
Multiple [200, 201, 202, 203, 204] |  Workload | Empirical | Yes | No | No |
SWAT and NASA TLX |  Workload | Surveyed Data | No | No | No | No
TAWL and TOSS [190] |  Workload | Task Network | Yes | No | No | No
Gao et al. [212] |  Trust | Stochastic process | Yes | Yes | No | No
Israelsen et al. [213] |  Trust | SEM | Yes | No | No | No
Martinie et al. [107] |  Tasks | Task Hierarchy | No | No | No | Yes
Task Analysis |  Tasks | Task Hierarchy | No | No | No | Yes
PAWS [232] |  Single Pilot Workload | Discrete-Event | Yes | ? | No | Yes
OMAR, IMPRINT, SAINT |  General Task + Workload | Discrete-Event | Yes | Yes | No | Yes
D-OMAR |  Distributed Pilot Task + Workload | Discrete-Event | Yes | Yes | No | Yes
Feng et al. [235] |  Mission Execution Time | Stochastic process | Yes | Yes | No | No
QN-MHRP from [220] |  Concurrent Tasks | Integrated | Yes | Yes | No | Yes
MIDAS |  Cockpit and ATC Interface | Integrated | Yes | Yes | No | Yes
ACT-R/IMPRINT |  General Purpose | Integrated | Yes | Yes | No | Yes
WMC [226] |  General Purpose | Integrated | Yes | ? | No | Yes

##  VI Conclusions and Recommendations

We provided an overview of human modeling including fundamental theories of
human cognition, decision-making, perception and actuation, as well as the
state-of-art human operator modeling and human factors techniques for
assessing human performance in aviation, and for the design, verification and
validation of human-machine systems.

We have found that human operator for human-_automation_ systems is much more
common than for human-_autonomy_ systems. By automation, we mean systems
helping humans to perform a limited set of tasks in a limited set of
environments. In this case, engineers can provide dedicate software programs
to handle each case. When the number of goals and environments makes this
standard approach impractical, then the system must include perception and
decision-making, and we refer to it as autonomy. In this latter case, there is
a need to reason about what the system and the human “know” about the
environment, what the system “believes” that the human “knows”, what the human
believes that the system knows, and so on. Also, we have found that, while
general purpose human models exist (such as cognitive architectural models),
they tend to be difficult to construct as they may require a considerable
knowledge capturing effort, they are rather brittle, and are not suitable for
systematic design, verification and validation of human-machine systems.

System-theoretic models, such as stochastic processes, are easier to
construct. However, they may not scale well to industrial-scale applications
and generalize poorly with respect to the task and the context. Formal methods
models have been primarily built for the analysis and verification of
interactions between human and existing automation. There is a lack of formal
modeling of human operator for assessing performance and capabilities in
scenarios involving the operation of autonomous systems including single-pilot
applications. Furthermore, the approaches we have surveyed tend to analyze the
combined human-machine system at one level of abstraction, hitting the well-
known state explosion problem.

Based on the outcomes of this survey, we feel that further research and
development efforts are required to deliver a unified framework for modeling
and verification of human-autonomy systems. We make the following
recommendations

_Declarative and compositional specifications._ Declarative modeling [239,
240] enables us to provide a description of the capabilities of the human
operator rather than details behind the mechanism which implements those
capabilities. The expected increase in the complexity of human-autonomy
systems makes testing and simulation less effective due to the large possible
set of environments to be considered. Declarative models enable _Formal
methods_ [241] are exhaustive and lead to strong guarantees on safety and/or
performance at the expense of computational complexity. Tractability problems
can be tackled with appropriate abstractions and compositional frameworks such
as contract-based design (CBD) [242]. One difficulty facing compositional
modeling of human operators is that workload measures of tasks are difficult
to compose. Typically, getting the workload of two or more tasks being
performed concurrently requires re-collecting workload ratings for the
combination of tasks being performed. Multiple-resource models provide a
somewhat limited computational way of composing workloads. However, those
compositional techniques are still experimental and have not been extensively
validated.

_New specification languages to account for different kinds of uncertainty and
time._ As machine exhibits more human-like traits such as using knowledge to
make complex decisions, there emerge a need to reason about not only about
what the system knows, but also what the human operator knows about the
system, and what the system knows about what the human operator knows about
the system, and so on. Modeling knowledge and higher order of belief can be
achieved using the framework provided by epistemic logic [135]. This framework
has been used, for instance, in [243]. Models of humans should be able to
describe the state of knowledge which includes what the human knows about the
knowledge (not the vivid facts) of the machine. There are several tools that
have appeared in the area of verification of epistemic dynamic systems (see
for example [244]) that could be used to perform formal verification. However,
the problem is in modeling the epistemic state in a declarative way. Moreover,
issues such as awareness [245, 246] has to be taken into account, and modeling
techniques and verification tools for modeling awareness seem to be lacking.
Furthermore, the declarative modeling language should mix epistemic modalities
with several others including temporal and probabilistic ones, leading to
verification problems that become intractable. Research in both areas of
modeling and decision procedures is needed to enable formal verification of
these new class of models.

_Human-factors, subject-matter experts, and engineering interfaces._ The
analysis of human-machine systems will require collaboration among several
experts in different areas such as human-factors (HF), subject-matter (SM),
and engineers (E). An integrated modeling and verification environment will
need to provide appropriate interfaces to all. HF and SM experts may not have
the appropriate background to build models amenable to formal analysis.
Similarly, they may not be able to interpret results generated by formal
verification tools.

Interpretability of analysis results by HF and SM experts will be essential
given the current state of research in human modeling as outlined in this
survey. There is a certain degree of model uncertainty that may lead to
incorrect analysis results. Thus, we believe that it is important to provide
the right level of explanation to experts in various field to assess the
results and identify potential modeling errors.

## References

  * [1] N. Kalra and S. M. Paddock, “Driving to safety: How many miles of driving would it take to demonstrate autonomous vehicle reliability?” _Transportation Research Part A: Policy and Practice_ , vol. 94, pp. 182–193, 2016, publisher: Elsevier.
  * [2] J. R. Boyd, _Destruction and creation_. US Army Comand and General Staff College, 1987.
  * [3] M. L. Bolton, E. J. Bass, and R. I. Siminiceanu, “Using formal verification to evaluate human-automation interaction: A review,” _IEEE Transactions on Systems, Man, and Cybernetics: Systems_ , vol. 43, no. 3, pp. 488–503, 2013.
  * [4] B. Weyers, J. Bowen, A. Dix, and P. Palanque, _The handbook of formal methods in human-computer interaction_. Springer, 2017.
  * [5] D. M. Green, J. A. Swets _et al._ , _Signal detection theory and psychophysics_. Wiley New York, 1966, vol. 1.
  * [6] T. D. Wickens, _Elementary signal detection theory_. Oxford University Press, USA, 2002.
  * [7] P. Verghese, “Visual search and attention: A signal detection theory approach,” vol. 31, pp. 523–535, 2001.
  * [8] M. P. Eckstein, J. P. Thomas, J. Palmer, and S. S. Shimozaki, “A signal detection model predicts the effects of set size on visual search accuracy for feature, conjunction, triple conjunction, and disjunction displays,” vol. 62, pp. 425–451, 2000.
  * [9] J. M. Wolfe and H. Pashler, “Visual search,” vol. 1, pp. 13–73, 1998.
  * [10] A. M. Treisman and G. Gelade, “A feature-integration theory of attention,” vol. 12, pp. 97–136, 1980.
  * [11] C. Bundesen, “A theory of visual attention,” vol. 97, p. 523, 1990.
  * [12] J. T. Townsend, “Serial vs. parallel processing: Sometimes they look like tweedledum and tweedledee but they can (and should) be distinguished,” vol. 1, pp. 46–54, 1990.
  * [13] D. Kahneman, _Attention and effort_. Citeseer, 1973, vol. 1063.
  * [14] C. D. Wickens, _Processing resources and attention_ , 1984.
  * [15] J. F. Lehman, J. E. Laird, P. Rosenbloom _et al._ , “A gentle introduction to soar, an architecture for human cognition,” _Invitation to cognitive science_ , vol. 4, pp. 212–249, 1996.
  * [16] H. A. Simon and E. A. Feigenbaum, “An information-processing theory of some effects of similarity, familiarization, and meaningfulness in verbal learning,” vol. 3, pp. 385–396, 1964.
  * [17] J. V. Neumann and O. Morgenstern, _Theory of games and economic behavior_. Princeton university press, 2007\.
  * [18] A. Tversky and D. Kahneman, “Advances in prospect theory: Cumulative representation of uncertainty,” vol. 5, pp. 297–323, 1992.
  * [19] G. Gigerenzer and R. Selten, _Bounded rationality: The adaptive toolbox_. MIT Press, 2002.
  * [20] G. Gigerenzer, U. Hoffrage, and H. Kleinbolting, “Probabilistic mental models: a brunswikian theory of confidence,” vol. 98, p. 506, 1991.
  * [21] G. Gigerenzer and D. G. Goldstein, “Reasoning the fast and frugal way: models of bounded rationality,” vol. 103, p. 650, 1996.
  * [22] G. Gigerenzer and P. M. Todd, _Simple heuristics that make us smart_. Oxford University Press, 1999.
  * [23] J. W. Payne, J. R. Bettman, and E. J. Johnson, _The adaptive decision maker_. Cambridge University Press, 1993\.
  * [24] H. A. Simon, “A behavioral model of rational choice,” _The quarterly journal of economics_ , vol. 69, no. 1, pp. 99–118, 1955.
  * [25] P. Reverdy, V. Srivastava, and N. E. Leonard, “Satisficing in multi-armed bandit problems,” _IEEE Transactions on Automatic Control_ , vol. 62, no. 8, pp. 3788–3803, 2017.
  * [26] E. Brunswik, _The conceptual framework of psychology_. University of Chicago Press, 1952.
  * [27] N. Karelaia and R. M. Hogarth, “Determinants of linear judgment: a meta-analysis of lens model studies,” vol. 134, p. 404, 2008.
  * [28] R. Hyman, “Stimulus information as a determinant of reaction time,” vol. 45, p. 188, 1953.
  * [29] W. E. Hick, “On the rate of gain of information,” vol. 4, pp. 11–26, 1952.
  * [30] P. M. Fitts, “The information capacity of the human motor system in controlling the amplitude of movement,” vol. 47, p. 381, 1954.
  * [31] I. S. MacKenzie, “Fitts’ law as a research and design tool in human-computer interaction,” vol. 7, pp. 91–139, 1992.
  * [32] W. R. Soukoreff and S. I. MacKenzie, “Towards a standard for pointing device evaluation, perspectives on 27 years of fitts’ law research in hci,” vol. 61, pp. 751–789, 2004.
  * [33] J. O. Wobbrock, E. Cutrell, S. Harada, and I. S. MacKenzie, “An error model for pointing based on fitts’ law.” Proceedings of the SIGCHI conference on human factors in computing systems, 2008\.
  * [34] J. Accot and S. Zhai, “Beyond fitts’ law: models for trajectory-based hci tasks.” 1997, Proceedings of the ACM SIGCHI Conference on Human factors in computing systems.
  * [35] S. Dekker and E. Hollnagel, “Human factors and folk models,” _Cognition, Technology & Work_, vol. 6, no. 2, pp. 79–86, 2004.
  * [36] N. Moray, _Mental workload: Its theory and measurement_. Springer Science & Business Media, 2013, vol. 8.
  * [37] D. Navon and D. Gopher, “On the economy of the human-processing system.” _Psychological review_ , vol. 86, no. 3, p. 214, 1979.
  * [38] T. B. Sheridan and R. Simpson, “Toward the definition and measurement of the mental workload of transport pilots,” Cambridge, Mass.: Massachusetts Institute of Technology, Dept. of …, Tech. Rep., 1979.
  * [39] D. Gopher and E. Donchin, “Workload: An examination of the concept.” 1986.
  * [40] G. B. Reid and T. E. Nygren, “The subjective workload assessment technique: A scaling procedure for measuring mental workload,” in _Advances in psychology_. Elsevier, 1988, vol. 52, pp. 185–218.
  * [41] Y.-Y. Yeh and C. D. Wickens, “Dissociation of performance and subjective measures of workload,” _Human Factors_ , vol. 30, no. 1, pp. 111–120, 1988\.
  * [42] D. Gopher and R. Braune, “On the psychophysics of workload: Why bother with subjective measures?” _Human Factors_ , vol. 26, no. 5, pp. 519–532, 1984\.
  * [43] C. D. Wickens and C. Kessel, “Processing resource demands of failure detection in dynamic systems.” _Journal of Experimental Psychology: Human Perception and Performance_ , vol. 6, no. 3, p. 564, 1980.
  * [44] H. R. Jex, “Measuring mental workload: Problems, progress, and promises,” in _Advances in psychology_. Elsevier, 1988, vol. 52, pp. 5–39.
  * [45] C. D. Wickens, “Processing resources and attention,” _Multiple-task performance_ , vol. 1991, pp. 3–34, 1991.
  * [46] J. B. Isreal, G. L. Chesney, C. D. Wickens, and E. Donchin, “P300 and tracking difficulty: Evidence for multiple resources in dual-task performance,” _Psychophysiology_ , vol. 17, no. 3, pp. 259–273, 1980.
  * [47] M. C. Polson and A. Friedman, “Task-sharing within and between hemispheres: A multiple-resources approach,” _Human factors_ , vol. 30, no. 5, pp. 633–643, 1988.
  * [48] A. Friedman and M. C. Polson, “Hemispheres as independent resource system: Limited-capacity processing and cerebral specialization.” _Journal of Experimental Psychology: Human Perception and Performance_ , vol. 7, no. 5, p. 1031, 1981.
  * [49] D. B. Boles and M. B. Law, “A simultaneous task comparison of differentiated and undifferentiated hemispheric resource theories.” _Journal of Experimental Psychology: Human Perception and Performance_ , vol. 24, no. 1, p. 204, 1998.
  * [50] H. Pashler, “Dual-task interference in simple tasks: data and theory.” _Psychological bulletin_ , vol. 116, no. 2, p. 220, 1994.
  * [51] M. C. Smith, “Theories of the psychological refractory period.” _Psychological bulletin_ , vol. 67, no. 3, p. 202, 1967.
  * [52] D. E. Meyer and D. E. Kieras, “A computational theory of executive cognitive processes and multiple-task performance: Part i. basic mechanisms,” vol. 104, p. 3, 1997.
  * [53] N. Meshkati, “Toward development of a cohesive model of workload,” in _Advances in Psychology_. Elsevier, 1988, vol. 52, pp. 305–314.
  * [54] M. S. Young and N. A. Stanton, “Malleable attentional resources theory: a new explanation for the effects of mental underload on performance,” _Human factors_ , vol. 44, no. 3, pp. 365–375, 2002.
  * [55] D. A. Sawin and M. W. Scerbo, “Effects of instruction type and boredom proneness in vigilance: Implications for boredom and workload,” _Human factors_ , vol. 37, no. 4, pp. 752–765, 1995.
  * [56] F. T. Eggemeier and G. F. Wilson, “Performance-based and subjective assessment of workload in multi-task environments,” _Multiple-task performance_ , pp. 217–278, 1991.
  * [57] S. G. Hart and C. D. Wickens, “Workload assessment and prediction,” in _Manprint_. Springer, 1990, pp. 257–296.
  * [58] M. R. Endsley and D. Garland, “Theoretical underpinnings of situation awareness: A critical review,” pp. 3–32, 2000.
  * [59] C. Dominguez, “Can sa be defined?” Tech. Rep., 1994.
  * [60] M. R. Endsley, “Toward a theory of situation awareness in dynamic systems,” vol. 37, pp. 32–64, 1995.
  * [61] C. E. Billings and W. D. Reynard, “Human factors in aircraft incidents: results of a 7-year study.” _Aviation, Space, and Environmental Medicine_ , vol. 55, no. 10, pp. 960–965, 1984.
  * [62] N. T. S. Board, “Runway overrun american airlines flight 2253 boeing 757-200, n668aa jackson hole, wyoming,” _NTSB Incident Report_ , 2012.
  * [63] K. Funk, B. Lyall, J. Wilson, R. Vint, M. Niemczyk, C. Suroteguh, and G. Owen, “Flight deck automation issues,” _The International Journal of Aviation Psychology_ , vol. 9, no. 2, pp. 109–123, 1999.
  * [64] E. Wiener, “Complacency: Is the term useful for air safety,” in _Proceedings of the 26th Corporate Aviation Safety Seminar_ , vol. 117, 1981, pp. 116–125.
  * [65] R. Parasuraman, T. B. Sheridan, and C. D. Wickens, “Situation awareness, mental workload, and trust in automation: Viable, empirically supported cognitive engineering constructs,” _Journal of cognitive engineering and decision making_ , vol. 2, no. 2, pp. 140–160, 2008.
  * [66] R. Parasuraman, R. Molloy, and I. L. Singh, “Performance consequences of automation-induced’complacency’,” _The International Journal of Aviation Psychology_ , vol. 3, no. 1, pp. 1–23, 1993.
  * [67] R. Parasuraman and D. H. Manzey, “Complacency and bias in human use of automation: An attentional integration,” _Human factors_ , vol. 52, no. 3, pp. 381–410, 2010.
  * [68] N. Moray and T. Inagaki, “Attention and complacency,” _Theoretical Issues in Ergonomics Science_ , vol. 1, no. 4, pp. 354–365, 2000.
  * [69] P. A. Hancock, “On the nature of vigilance,” _Human factors_ , vol. 59, no. 1, pp. 35–43, 2017.
  * [70] J. S. Warm, R. Parasuraman, and G. Matthews, “Vigilance requires hard mental work and is stressful,” _Human factors_ , vol. 50, no. 3, pp. 433–441, 2008\.
  * [71] M. L. Cummings, F. Gao, and K. M. Thornburg, “Boredom in the workplace: A new look at an old problem,” _Human factors_ , vol. 58, no. 2, pp. 279–300, 2016\.
  * [72] R. P. Smith, “Boredom: A review,” _Human factors_ , vol. 23, no. 3, pp. 329–340, 1981.
  * [73] L. J. Prinzel III and F. G. Freeman, “Task-specific sex differences in vigilance performance: subjective workload and boredom,” _Perceptual and motor skills_ , vol. 85, no. 3_suppl, pp. 1195–1202, 1997.
  * [74] E. L. Wiener and D. C. Nagel, _Human factors in aviation_. Gulf Professional Publishing, 1988.
  * [75] B. Barber, “The logic and limits of trust,” 1983.
  * [76] T. B. Sheridan and R. T. Hennessy, “Research and modeling of supervisory control behavior. report of a workshop,” NATIONAL RESEARCH COUNCIL WASHINGTON DC COMMITTEE ON HUMAN FACTORS, Tech. Rep., 1984.
  * [77] B. M. Muir, “Trust between humans and machines, and the design of decision aids,” _International journal of man-machine studies_ , vol. 27, no. 5-6, pp. 527–539, 1987.
  * [78] J. Lee and N. Moray, “Trust, control strategies and allocation of function in human-machine systems,” _Ergonomics_ , vol. 35, no. 10, pp. 1243–1270, 1992\.
  * [79] J. D. Lee and N. Moray, “Trust, self-confidence, and operators’ adaptation to automation,” _International journal of human-computer studies_ , vol. 40, no. 1, pp. 153–184, 1994.
  * [80] B. M. Muir, “Trust in automation: Part i. theoretical issues in the study of trust and human intervention in automated systems,” _Ergonomics_ , vol. 37, no. 11, pp. 1905–1922, 1994.
  * [81] B. M. Muir and N. Moray, “Trust in automation. part ii. experimental studies of trust and human intervention in a process control simulation,” _Ergonomics_ , vol. 39, no. 3, pp. 429–460, 1996.
  * [82] M. S. Cohen, R. Parasuraman, and J. T. Freeman, “Trust in decision aids: A model and its training implications,” in _in Proc. Command and Control Research and Technology Symp_. Citeseer, 1998.
  * [83] E. Hollnagel, “The phenotype of erroneous actions,” _International Journal of Man-Machine Studies_ , vol. 39, no. 1, pp. 1–32, 1993.
  * [84] D. A. Wiegmann and S. A. Shappell, “Applying the human factors analysis and classification system (hfacs) to the analysis of commercial aviation accident data,” 2001.
  * [85] J. Reason, _Human error_. Cambridge university press, 1990.
  * [86] R. L. Helmreich, “On error management: lessons from aviation,” _Bmj_ , vol. 320, no. 7237, pp. 781–785, 2000.
  * [87] B. L. Hooey and D. C. Foyle, “A post hoc analysis of navigation errors during surface operations: Identifi cation of contributing factors and mitigating solutions,” in _Ohio State University_. Citeseer, 2001.
  * [88] C.-C. Chou, D. Madhavan, and K. Funk, “Studies of cockpit task management errors,” _The International Journal of Aviation Psychology_ , vol. 6, no. 4, pp. 307–320, 1996.
  * [89] S. S. Silva and R. J. Hansman, “Divergence between flight crew mental model and aircraft system state in auto-throttle mode confusion accident and incident cases,” _Journal of cognitive engineering and decision making_ , vol. 9, no. 4, pp. 312–328, 2015.
  * [90] J. Bredereke and A. Lankenau, “A rigorous view of mode confusion,” in _International Conference on Computer Safety, Reliability, and Security_. Springer, 2002, pp. 19–31.
  * [91] N. Leveson, L. D. Pinnel, S. D. Sandys, S. Koga, and J. D. Reese, “Analyzing software specifications for mode confusion potential,” in _Proceedings of a workshop on human error and system development_. Glasgow Accident Analysis Group, 1997, pp. 132–146.
  * [92] E. M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith, _Model checking_. MIT press, 2018.
  * [93] T. Nipkow, L. C. Paulson, and M. Wenzel, _Isabelle/HOL: a proof assistant for higher-order logic_. Springer Science & Business Media, 2002, vol. 2283.
  * [94] M. L. Bolton, E. J. Bass, and R. I. Siminiceanu, “Using formal verification to evaluate human-automation interaction: A review,” vol. 43, pp. 488–503, 2013\.
  * [95] E. L. Gunter, A. Yasmeen, C. A. Gunter, and A. Nguyen, “Specifying and analyzing workflows for automated identification and data capture,” in _2009 42nd Hawaii International Conference on System Sciences_. IEEE, 2009, pp. 1–11.
  * [96] S. Basnyat, P. Palanque, B. Schupp, and P. Wright, “Formal socio-technical barrier modelling for safety-critical interactive systems design,” _Safety Science_ , vol. 45, no. 5, pp. 545–565, 2007.
  * [97] F. Paterno, C. Mancini, and S. Meniconi, “Concurtasktrees: A diagrammatic notation for specifying task models,” in _Human-computer interaction INTERACT 97_. Springer, 1997, pp. 362–369.
  * [98] C. M. Mitchell and R. A. Miller, “A discrete control model of operator function: A methodology for information display design,” _IEEE Transactions on Systems, Man, and Cybernetics_ , vol. 16, no. 3, pp. 343–357, 1986\.
  * [99] M. L. Bolton and E. J. Bass, “Enhanced operator function model: A generic human task behavior modeling language,” in _2009 IEEE International Conference on Systems, Man and Cybernetics_. IEEE, 2009, pp. 2904–2911.
  * [100] D. Hix and H. R. Hartson, _Developing user interfaces: Ensuring usability through product and process_. Wiley, 1993\.
  * [101] P. Palanque, R. Bastide, and V. Sengès, “Validating interactive system design through the verification of formal task and system models,” in _IFIP International Conference on Engineering for Human-Computer Interaction_. Springer, 1995, pp. 189–212.
  * [102] Y. Ait-Ameur and M. Baron, “Formal and experimental validation approaches in hci systems design based on a shared event b model,” _International Journal on Software Tools for Technology Transfer_ , vol. 8, no. 6, pp. 547–563, 2006.
  * [103] M. L. Bolton, R. I. Siminiceanu, and E. J. Bass, “A systematic approach to model checking human–automation interaction using task analytic models,” _IEEE Transactions on Systems, Man, and Cybernetics-Part A: Systems and Humans_ , vol. 41, no. 5, pp. 961–976, 2011.
  * [104] Y. A. Ameur, M. Baron, and P. Girard, “Formal validation of hci user tasks.” in _Software engineering research and practice_ , 2003, pp. 732–738.
  * [105] F. Paternò, C. Santoro, and S. Tahmassebi, “Formal models for cooperative tasks: concepts and an application for en-route air traffic control,” in _Design, Specification and Verification of Interactive Systems’ 98_. Springer, 1998, pp. 71–86.
  * [106] E. J. Bass, M. L. Bolton, K. Feigh, D. Griffith, E. Gunter, W. Mansky, and J. Rushby, “Toward a multi-method approach to formalizing human-automation interaction and human-human communications,” in _2011 IEEE International Conference on Systems, Man, and Cybernetics_. IEEE, 2011, pp. 1817–1824.
  * [107] C. Martinie and P. Palanque, “Fine grain modeling of task deviations for assessing qualitatively the impact of both system failures and human error on operator performance,” 2014.
  * [108] A. Cerone, P. A. Lindsay, and S. Connelly, “Formal analysis of human-computer interaction using model-checking,” in _Third IEEE International Conference on Software Engineering and Formal Methods (SEFM’05)_. IEEE, 2005, pp. 352–361.
  * [109] P. Lindsay and S. Connelly, “Modelling erroneous operator behaviours for an air-traffic control task,” in _Australian Computer Science Communications_ , vol. 24, no. 4. Australian Computer Society, Inc., 2002, pp. 43–54.
  * [110] A. Blandford, R. Butterworth, and P. Curzon, “Models of interactive systems: a case study on programmable user modelling,” _International Journal of Human-Computer Studies_ , vol. 60, no. 2, pp. 149–200, 2004.
  * [111] R. Butterworth, A. Blandford, and D. Duke, “The role of formal proof in modelling interactive behaviour,” in _Design, Specification and Verification of Interactive Systems’ 98_. Springer, 1998, pp. 87–101.
  * [112] ——, “Demonstrating the cognitive plausibility of interactive system specifications,” _Formal Aspects of Computing_ , vol. 12, no. 4, pp. 237–259, 2000.
  * [113] R. Rukšėnas, P. Curzon, J. Back, and A. Blandford, “Formal modelling of cognitive interpretation,” in _International Workshop on Design, Specification, and Verification of Interactive Systems_. Springer, 2006, pp. 123–136.
  * [114] R. Rukšėnas, J. Back, P. Curzon, and A. Blandford, “Verification-guided modelling of salience and cognitive load,” _Formal Aspects of Computing_ , vol. 21, no. 6, p. 541, 2009.
  * [115] P. Masci, P. Curzon, A. Blandford, and D. Furniss, “Modelling distributed cognition systems in pvs,” _Electronic Communications of the EASST_ , vol. 45, 2011.
  * [116] S. Owre, J. Rushby, and N. Shankar, “PVS: A prototype verification system,” in _Automated Deduction_ , ser. Lecture Notes in Computer Science, D. Kapur, Ed. Springer Berlin / Heidelberg, 1992, vol. 607, pp. 748–752.
  * [117] N. V. Flor and E. L. Hutchins, “Analyzing distributed cognition in software teams: A case study of team programming during,” in _Empirical studies of programmers: Fourth workshop_. Intellect Books, 1991, p. 36.
  * [118] N. A. Neogi, “Capturing safety requirements to enable effective task allocation between humans and automaton in increasingly autonomous systems.” 16th AIAA Aviation Technology, Integration, and Operations Conference, 2016.
  * [119] J. Moore, R. Ivie, T. Gledhill, E. Mercer, and M. A. Goodrich, “Modeling human workload in unmanned aerial systems,” in _2014 AAAI Spring Symposium Series_ , 2014.
  * [120] A. Houser, L. M. Ma, K. M. Feigh, and M. L. Bolton, “Using formal methods to reason about taskload and resource conflicts in simulated air traffic scenarios,” _Innovations in Systems and Software Engineering_ , vol. 14, no. 1, pp. 1–14, 2018.
  * [121] A. Joshi, S. P. Miller, and M. P. Heimdahl, “Mode confusion analysis of a flight guidance system using formal methods,” in _Digital Avionics Systems Conference, 2003. DASC’03. The 22nd_ , vol. 1. IEEE, 2003, pp. 2–D.
  * [122] R. W. Butler, S. P. Miller, J. N. Potts, and V. A. Carreno, “A formal methods approach to the analysis of mode confusion,” in _17th DASC. AIAA/IEEE/SAE. Digital Avionics Systems Conference. Proceedings (Cat. No. 98CH36267)_ , vol. 1. IEEE, 1998, pp. C41–1.
  * [123] J. C. Campos and M. Harrison, “Modelling and analysing the interactive behaviour of an infusion pump,” _Electronic Communications of the EASST_ , vol. 45, 2011.
  * [124] J. Rushby, “Using model checking to help discover mode confusions and other automation surprises,” _Reliability Engineering & System Safety_, vol. 75, no. 2, pp. 167–177, 2002.
  * [125] A. Degani and M. Heymann, “Pilot-autopilot interaction: A formal perspective,” _Abbott et al.[1]_ , pp. 157–168, 2000.
  * [126] D. Javaux, “A method for predicting errors when interacting with finite state systems. how implicit learning shapes the user’s knowledge of a system,” _Reliability Engineering & System Safety_, vol. 75, no. 2, pp. 147–165, 2002.
  * [127] J. Crow, D. Javaux, and J. Rushby, “Models and mechanized methods that integrate human factors into automation design,” in _International Conference on Human-Computer Interaction in Aeronautics: HCI-Aero_. Tolosa Press Toulouse, France, 2000, pp. 163–168.
  * [128] S. Combéfis, D. Giannakopoulou, and C. Pecheur, “Automatic detection of potential automation surprises for adept models,” _IEEE Transactions on Human-Machine Systems_ , vol. 46, no. 2, pp. 267–278, 2015.
  * [129] R. Bastide and S. Basnyat, “Error patterns: Systematic investigation of deviations in task models,” in _International Workshop on Task Models and Diagrams for User Interface Design_. Springer, 2006, pp. 109–121.
  * [130] M. L. Bolton, E. J. Bass, and R. I. Siminiceanu, “Using formal methods to predict human error and system failures,” in _Proceedings of the 2nd Applied Human Factors and Ergonomics International Conference_ , 2008, pp. 14–17.
  * [131] M. L. Bolton and E. J. Bass, “Formal modeling of erroneous human behavior and its implications for model checking,” in _Proc. 6th NASA Langley Formal Methods Workshop_. Citeseer, 2008, pp. 62–64.
  * [132] M. L. Bolton, “A task-based taxonomy of erroneous human behavior,” _International Journal of Human-Computer Studies_ , vol. 108, pp. 105–121, 2017.
  * [133] M. L. Bolton, K. A. Molinaro, and A. M. Houser, “A formal method for assessing the impact of task-based erroneous human behavior on system safety,” _Reliability Engineering & System Safety_, vol. 188, pp. 168–180, 2019\.
  * [134] M. L. Bolton, X. Zheng, and E. Kang, “A formal method for including the probability of erroneous human task behavior in system analyses,” _Reliability Engineering & System Safety_, vol. 213, p. 107764, 2021.
  * [135] R. Fagin, J. Y. Halpern, Y. Moses, and M. Vardi, _Reasoning about knowledge_. MIT press, 2004.
  * [136] S. A. Kripke, “Semantical analysis of modal logic i normal modal propositional calculi,” _Mathematical Logic Quarterly_ , vol. 9, no. 5-6, pp. 67–96, 1963\.
  * [137] W. Van Der Hoek and M. Wooldridge, “Model checking knowledge and time,” in _International SPIN Workshop on Model Checking of Software_. Springer, 2002, pp. 95–111.
  * [138] M. Kacprzak, A. Lomuscio, and W. Penczek, “Verification of multiagent systems via unbounded model checking,” in _Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems-Volume 2_. IEEE Computer Society, 2004, pp. 638–645.
  * [139] L. Wu, K. Su, and Q. Chen, “Model checking temporal logics of knowledge and its application in security verification,” in _International Conference on Computational and Information Science_. Springer, 2005, pp. 349–354.
  * [140] A. Lomuscio, H. Qu, and F. Raimondi, “Mcmas: an open-source model checker for the verification of multi-agent systems,” pp. 1–22, 2015.
  * [141] W. Penczek and A. Lomuscio, “Verifying epistemic properties of multi-agent systems via bounded model checking.” Proceedings of the second international joint conference on Autonomous agents and multiagent systems, 2003.
  * [142] J. Hintikka, “Impossible possible worlds vindicated,” in _Game-theoretical semantics_. Springer, 1979, pp. 367–379.
  * [143] J. Y. Halpern, Y. Moses, and M. Y. Vardi, “Algorithmic knowledge,” in _Theoretical Aspects of Reasoning about Knowledge_. Elsevier, 1994, pp. 255–266.
  * [144] R. Fagin, J. Y. Halpern, and M. Y. Vardi, “A nonstandard approach to the logical omniscience problem,” _Artificial Intelligence_ , vol. 79, no. 2, pp. 203–240, 1995.
  * [145] H. V. Ditmarsch, A. Herzig, J. Lang, and P. Marquis, “Introspective forgetting,” vol. 169, pp. 405–423, 2009.
  * [146] G. Primiero, F. Raimondi, and N. Rungta, “Model checking degrees of belief in a system of agents.” Proceedings of the 2014 international conference on Autonomous agents and multi-agent systems, 2014.
  * [147] S. Ahrenbach and A. Goodloe, “Formal analysis of pilot error with agent safety logic,” _Innovations in systems and software engineering_ , vol. 14, no. 1, pp. 47–58, 2018.
  * [148] The Coq development team, _The Coq proof assistant reference manual_ , LogiCal Project, 2012, version 8.4. [Online]. Available: http://coq.inria.fr
  * [149] M. D. Fleetwood and M. D. Byrne, “Modeling the visual search of displays: a revised act-r model of icon search based on eye-tracking data,” vol. 21, pp. 153–197, 2006.
  * [150] L. Itti, C. Koch, E. Niebur, and Others, “A model of saliency-based visual attention for rapid scene analysis,” vol. 20, pp. 1254–1259, 1998.
  * [151] B. J. Melloy, S. Das, A. K. Gramopadhye, and A. T. Duchowski, “A model of extended, semisystematic visual search,” vol. 48, pp. 540–554, 2006.
  * [152] C. Koch and S. Ullman, _Shifts in selective visual attention: towards the underlying neural circuitry_. Springer, 1987.
  * [153] K. G. Thompson and N. P. Bichot, “A visual salience map in the primate frontal eye field,” vol. 147, pp. 249–262, 2005.
  * [154] X. Hou and L. Zhang, “Saliency detection: A spectral residual approach.” IEEE Conference on Computer Vision and Pattern Recognition, 2007, pp. 1–8.
  * [155] C. D. Wickens, J. Helleberg, J. Goh, X. Xu, and W. J. Horrey, “Pilot task management: Testing an attentional expected value model of visual scanning,” Tech. Rep., 2001.
  * [156] C. D. Wickens, “Noticing events in the visual workplace: The seev and nseev models.” 2015.
  * [157] W. J. Horrey, C. D. Wickens, and K. Consalus, “Modeling drivers’ visual attention allocation while interacting with in-vehicle technologies,” vol. 12, p. 67, 2006.
  * [158] N. D. Cassavaugh, A. Bos, C. McDonald, P. Gunaratne, and R. W. Backs, “Assessment of the seev model to predict attention allocation at intersections during simulated driving.” Proceedings of the Seventh International Driving Symposium on Human Factors in Driver Assessment, Training, and Vehicle Design, 2013.
  * [159] A. Krizhevsky, I. Sutskever, and G. E. Hinton, “Imagenet classification with deep convolutional neural networks,” _Advances in neural information processing systems_ , vol. 25, 2012.
  * [160] K. He, X. Zhang, S. Ren, and J. Sun, “Deep residual learning for image recognition,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2016, pp. 770–778.
  * [161] K. He, G. Gkioxari, P. Dollár, and R. Girshick, “Mask r-cnn,” in _Proceedings of the IEEE international conference on computer vision_ , 2017, pp. 2961–2969.
  * [162] J. Deng, W. Dong, R. Socher, L.-J. Li, K. Li, and L. Fei-Fei, “Imagenet: A large-scale hierarchical image database,” in _2009 IEEE conference on computer vision and pattern recognition_. Ieee, 2009, pp. 248–255.
  * [163] J. Sweller, J. J. Van Merrienboer, and F. G. Paas, “Cognitive architecture and instructional design,” _Educational psychology review_ , vol. 10, no. 3, pp. 251–296, 1998.
  * [164] D. C. Foyle, B. L. Hooey, M. D. Byrne, K. M. Corker, S. Deutsch, C. Lebiere, K. Leiden, and C. D. Wickens, “Human performance models of pilot behavior,” in _Proceedings of the Human Factors and Ergonomics Society Annual Meeting_ , vol. 49, no. 12. SAGE Publications Sage CA: Los Angeles, CA, 2005, pp. 1109–1113.
  * [165] K. A. Gluck and R. W. Pew, _Modeling human behavior with integrated cognitive architectures: Comparison, evaluation, and validation_. Psychology Press, 2006.
  * [166] C. Lebiere and J. R. Anderson, _The atomic components of thought_. Lawrence Erlbaum, 1998.
  * [167] J. E. Laird, _The Soar cognitive architecture_. MIT Press, 2012.
  * [168] _Unified theories of cognition and the role of Soar_ , 1992.
  * [169] F. Gobet, P. C. Lane, S. Croker, P. C. Cheng, G. Jones, I. Oliver, and J. M. Pine, “Chunking mechanisms in human learning,” vol. 5, pp. 236–243, 2001.
  * [170] Pat and D. L. Choi, “A unified cognitive architecture for physical agents,” vol. 21, p. 1469, 2006.
  * [171] S. W. Tyler, C. Neukom, M. Logan, and J. Shively, “The midas human performance model,” in _Proceedings of the Human Factors and Ergonomics Society Annual Meeting_ , vol. 42, no. 3. SAGE Publications Sage CA: Los Angeles, CA, 1998, pp. 320–324.
  * [172] S. K. Card, A. Newell, and T. P. Moran, “The psychology of human-computer interaction,” 1983.
  * [173] _A GOMS analysis of the advanced automated cockpit_ , 1994.
  * [174] N. A. Taatgen, “A model of individual differences in skill acquisition in the kanfer–ackerman air traffic control task,” vol. 3, pp. 103–112, 2002.
  * [175] J. R. Anderson, D. Bothell, M. D. Byrne, S. Douglass, C. Lebiere, and Y. Qin, “An integrated theory of the mind,” vol. 111, p. 1036, 2004.
  * [176] K. R. Hammond, C. J. Hursch, and F. J. Todd, “Analyzing the components of clinical inference,” vol. 71, p. 438, 1964.
  * [177] A. M. Bisantz and A. R. Pritchett, “Measuring the fit between human judgments and automated alerting algorithms: A study of collision detection,” vol. 45, pp. 266–280, 2003.
  * [178] M. R. Endsley, “The application of human factors to the development of expert systems for advanced cockpits,” in _Proceedings of the Human Factors Society Annual Meeting_ , vol. 31, no. 12. SAGE Publications Sage CA: Los Angeles, CA, 1987, pp. 1388–1392.
  * [179] J. R. Busemeyer and J. T. Townsend, “Decision field theory: a dynamic-cognitive approach to decision making in an uncertain environment.” _Psychological review_ , vol. 100, no. 3, p. 432, 1993.
  * [180] W. P. Niedringhaus, “The jet: Wise model of national air space system evolution,” vol. 80, pp. 45–58, 2004.
  * [181] M. J. Kochenderfer, L. P. Espindle, J. K. Kuchar, and J. D. Griffith, “A comprehensive aircraft encounter model of the national airspace system,” vol. 17, pp. 41–53, 2008.
  * [182] C. Tomlin, G. J. Pappas, and S. Sastry, “Conflict resolution for air traffic management: A study in multiagent hybrid systems,” vol. 43, pp. 509–521, 1998\.
  * [183] A. R. Pritchett, S. Lee, and D. Goldsman, “Hybrid-system simulation for national airspace system safety analysis,” vol. 38, pp. 835–840, 2001.
  * [184] A. Pentland and A. Liu, “Modeling and prediction of human behavior,” vol. 11, pp. 229–242, 1999.
  * [185] J. R. Busemeyer, Z. Wang, and J. T. Townsend, “Quantum dynamics of human decision-making,” _Journal of Mathematical Psychology_ , vol. 50, no. 3, pp. 220–241, 2006.
  * [186] J. M. Schraagen, S. F. Chipman, and V. L. Shalin, _Cognitive task analysis_. Psychology Press, 2000.
  * [187] K. Leiden, J. Keller, and J. French, “Information to support the human performance modeling of a b757 flight crew during approach and landing,” _NASA Ames Research Center, Moffett Field, CA_ , 2002.
  * [188] T. L. Seamster and R. E. Redding, _Applied cognitive task analysis in aviation_. Routledge, 2017.
  * [189] S. Deutsch, R. W. Pew _et al._ , “Single pilot commercial aircraft operation,” _BBN Report 8436_ , 2005.
  * [190] D. B. Hamilton and C. R. Bierbaum, “Task analysis/workload (tawl): A methodology for predicting operator workload,” in _Proceedings of the Human Factors Society Annual Meeting_ , vol. 34, no. 16. SAGE Publications Sage CA: Los Angeles, CA, 1990, pp. 1117–1121.
  * [191] D. K. Mitchell, “Mental workload and arl workload modeling tools,” Army Research Lab Aberdeen Proving Ground MD, Tech. Rep., 2000.
  * [192] K. J. Sarno, “Role of multiple resources in predicting time-sharing efficiency: Evaluation of three workload models in a multiple-task setting,” _The International journal of aviation psychology_ , vol. 5, no. 1, pp. 107–130, 1995.
  * [193] C. D. Wickens, “Multiple resources and performance prediction,” _Theoretical issues in ergonomics science_ , vol. 3, no. 2, pp. 159–177, 2002\.
  * [194] W. J. Horrey and C. D. Wickens, “Multiple resource modeling of task interference in vehicle control, hazard awareness and in-vehicle task performance,” 2003.
  * [195] S. Jo, R. Myung, and D. Yoon, “Quantitative prediction of mental workload with the act-r cognitive architecture,” _International Journal of Industrial Ergonomics_ , vol. 42, no. 4, pp. 359–370, 2012.
  * [196] C. D. Wickens, J. Goh, J. Helleberg, W. J. Horrey, and D. A. Talleur, “Attentional models of multitask pilot performance using advanced display technology,” _Human factors_ , vol. 45, no. 3, pp. 360–380, 2003.
  * [197] H. A. P. Blom, J. Daams, and H. B. Nijhuis, _Human cognition modelling in air traffic management safety assessment_. NLR, 2001.
  * [198] N. Meshkati and A. Loewenthal, “An eclectic and critical review of four primary mental workload assessment methods: A guide for developing a comprehensive model,” in _Advances in Psychology_. Elsevier, 1988, vol. 52, pp. 251–267.
  * [199] S. G. Hart and L. E. Staveland, “Development of nasa-tlx (task load index): Results of empirical and theoretical research,” in _Advances in psychology_. Elsevier, 1988, vol. 52, pp. 139– 183.
  * [200] C. Dussault, J.-C. Jouanin, M. Philippe, and C.-Y. Guezennec, “Eeg and ecg changes during simulator operation reflect mental workload and vigilance,” _Aviation, space, and environmental medicine_ , vol. 76, no. 4, pp. 344–351, 2005.
  * [201] S. T. Iqbal, X. S. Zheng, and B. P. Bailey, “Task-evoked pupillary response to mental workload in human-computer interaction,” in _CHI’04 extended abstracts on Human factors in computing systems_. ACM, 2004, pp. 1477–1480.
  * [202] P. G. Jorna, “Spectral analysis of heart rate and psychological state: A review of its validity as a workload index,” _Biological psychology_ , vol. 34, no. 2-3, pp. 237–257, 1992.
  * [203] J. G. May, R. S. Kennedy, M. C. Williams, W. P. Dunlap, and J. R. Brannan, “Eye movement indices of mental workload,” _Acta psychologica_ , vol. 75, no. 1, pp. 75–89, 1990.
  * [204] K. J. Vicente, D. C. Thornton, and N. Moray, “Spectral analysis of sinus arrhythmia: A measure of mental effort,” _Human factors_ , vol. 29, no. 2, pp. 171–182, 1987.
  * [205] R. J. Shively, M. Brickner, and J. Silbiger, “A computational model of situational awareness instantiated in midas.” International Symposium on Aviation Psychology, 1997.
  * [206] J. S. McCarley, C. D. Wickens, J. Goh, and W. J. Horrey, “A computational model of attention/situation awareness.” Proceedings of the Human Factors and Ergonomics Society Annual Meeting, 2002.
  * [207] C. D. Wickens, J. S. McCarley, A. L. Alexander, L. C. Thomas, M. Ambinder, and S. Zheng, “Attention-situation awareness (a-sa) model of pilot error,” pp. 213–239, 2008.
  * [208] D. A. Wiegmann, A. Rich, and H. Zhang, “Automated diagnostic aids: The effects of aid reliability on users’ trust and reliance,” _Theoretical Issues in Ergonomics Science_ , vol. 2, no. 4, pp. 352–367, 2001.
  * [209] A. M. Bisantz and Y. Seong, “Assessment of operator trust in and utilization of automated decision-aids under different framing conditions,” _International Journal of Industrial Ergonomics_ , vol. 28, no. 2, pp. 85–97, 2001.
  * [210] M. Yeh and C. D. Wickens, “Display signaling in augmented reality: Effects of cue reliability and image realism on attention allocation and trust calibration,” _Human Factors_ , vol. 43, no. 3, pp. 355–365, 2001.
  * [211] J. D. Lee and K. A. See, “Trust in automation: Designing for appropriate reliance,” _Human factors_ , vol. 46, no. 1, pp. 50–80, 2004.
  * [212] J. Gao and J. D. Lee, “Extending the decision field theory to model operators’ reliance on automation in supervisory control situations,” _IEEE Transactions on Systems, Man, and Cybernetics-Part A: Systems and Humans_ , vol. 36, no. 5, pp. 943–959, 2006.
  * [213] B. Israelsen, P. Wu, K. Woodruff, G. Avdic-McIntire, A. Radlbeck, A. McLean, P. D. Highland, T. M. Schnell, and D. A. Javorsek, “Introducing smrtt: A structural equation model of multimodal real-time trust,” in _Companion of the 2021 ACM/IEEE International Conference on Human-Robot Interaction_ , 2021, pp. 126–130.
  * [214] R. H. Hoyle, “The structural equation modeling approach: Basic concepts and fundamental issues.” 1995.
  * [215] S. L. Morgan and C. Winship, _Counterfactuals and causal inference_. Cambridge University Press, 2015.
  * [216] D. Mitchell, C. Samms, M. Glumm, A. Krausman, M. Brelsford, and L. Garrett, “Improved performance research integration tool (imprint) model analyses in support of the situational understanding as an enabler for unit of action maneuver team soldiers science and technology objective (sto) in support of future combat systems.” Tech. Rep., 2004.
  * [217] A. B. Pritsker, D. B. Wortman, C. S. Seum, G. P. Chubb, and D. J. Seifert, “Saint: Volume i. systems analysis of integrated network of tasks,” Tech. Rep., 1974.
  * [218] C. Lebiere, R. Archer, W. Warwick, and D. Schunk, “Integrating modeling and simulation into a general-purpose tool.” Proceedings of the 11th International Conference on Human-Computer Interaction, 2005.
  * [219] K. R. Laughery, C. Lebiere, and S. Archer, “Modeling human performance in complex systems,” pp. 964–996, 2006.
  * [220] Y. Liu, R. Feyen, and O. Tsimhoni, “Queueing network-model human processor (qn-mhp): A computational architecture for multitask performance in human-machine systems,” vol. 13, pp. 37–70, 2006.
  * [221] S. W. Tyler, C. Neukom, M. Logan, and J. Shively, “The midas human performance model,” vol. 42, pp. 320–324, 1998.
  * [222] S. Deutsch and M. Adams, “The operator model architecture and its psychological framework.” Proceedings of the 6th IFAC Symposium on Man-Machine Systems, 1996.
  * [223] K. Leiden and B. Best, _A cross-model comparison of human performance modeling tools applied to aviation safety_. NASA, 2005.
  * [224] D. C. Foyle and B. L. Hooey, _Human performance modeling in aviation_. CRC Press, 2007.
  * [225] A. R. Pritchett, S. Y. Kim, and K. M. Feigh, “Modeling human–automation function allocation,” _Journal of cognitive engineering and decision making_ , vol. 8, no. 1, pp. 33–51, 2014.
  * [226] A. R. Pritchett, K. M. Feigh, S. Y. Kim, and S. K. Kannan, “Work models that compute to describe multiagent concepts of operation: Part 1,” _Journal of Aerospace Information Systems_ , vol. 11, no. 10, pp. 610–622, 2014.
  * [227] D. W. Lee, D. W. Fitzick, and E. J. Bass, “Simulating human performance of task sharing: Modeling task delay and delegation of authority,” in _Proceedings of the Human Factors and Ergonomics Society Annual Meeting_ , vol. 61, no. 1. SAGE Publications Sage CA: Los Angeles, CA, 2017, pp. 786–790.
  * [228] L. Haworth, C. C. Bivens, and R. Shively, “An investigation of single-piloted advanced cockpit and control configurations for nap-of-the-earth helicopter combat mission tasks,” in _American Helicopter Society, Annual Forum, 42 nd, Washington, DC_ , 1986, pp. 657–672.
  * [229] D. Harris, “A human-centred design agenda for the development of single crew operated commercial aircraft,” _Aircraft Engineering and Aerospace Technology_ , vol. 79, no. 5, pp. 518–526, 2007.
  * [230] S. Deutsch and R. Pew, “Modeling human error in a real-world teamwork environment,” in _Proceedings of the Annual Meeting of the Cognitive Science Society_ , vol. 24, no. 24, 2002.
  * [231] M. D. Byrne and A. Kirlik, “Using computational cognitive modeling to diagnose possible sources of aviation error,” _The international journal of aviation psychology_ , vol. 15, no. 2, pp. 135–155, 2005.
  * [232] A. J. Stimpson, J. C. Ryan, and M. L. Cummings, “Assessing pilot workload in single-pilot operations with advanced autonomy,” in _Proceedings of the Human Factors and Ergonomics Society Annual Meeting_ , vol. 60, no. 1. SAGE Publications Sage CA: Los Angeles, CA, 2016, pp. 675–679.
  * [233] C. A. Wolter and B. F. Gore, “A validated task analysis of the single pilot operations concept,” 2015.
  * [234] M. L. Cummings and S. Guerlain, “Developing operator capacity estimates for supervisory control of autonomous vehicles,” _Human factors_ , vol. 49, no. 1, pp. 1–15, 2007.
  * [235] L. Feng, C. Wiltsche, L. Humphrey, and U. Topcu, “Controller synthesis for autonomous systems interacting with human operators,” in _Proceedings of the acm/ieee sixth international conference on cyber-physical systems_. ACM, 2015, pp. 70–79.
  * [236] Y. Boussemart and M. Cummings, “Behavioral recognition and prediction of an operator supervising multiple heterogeneous unmanned vehicles,” _Humans operating unmanned systems_ , 2008.
  * [237] Y. Boussemart and M. L. Cummings, “Predictive models of human supervisory control behavioral patterns using hidden semi-markov models,” _Engineering Applications of Artificial Intelligence_ , vol. 24, no. 7, pp. 1252–1262, 2011.
  * [238] C. Wickens, J. McCarley, and K. Steelman-Allen, “Nt-seev: A model of attention capture and noticing on the flight deck,” in _Proceedings of the human factors and ergonomics society annual meeting_ , vol. 53, no. 12. SAGE Publications Sage CA: Los Angeles, CA, 2009, pp. 769–773.
  * [239] R. Kowalski, “Algorithm= logic+ control,” _Communications of the ACM_ , vol. 22, no. 7, pp. 424–436, 1979.
  * [240] D. Fahland, D. Lübke, J. Mendling, H. Reijers, B. Weber, M. Weidlich, and S. Zugal, “Declarative versus imperative process modeling languages: The issue of understandability,” in _Enterprise, Business-Process and Information Systems Modeling_. Springer, 2009, pp. 353–366.
  * [241] D. Peled, _Software Reliability Methods_ , ser. Texts in Computer Science. Springer, 2001.
  * [242] A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-B. Raclet, P. Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T. A. Henzinger, K. G. Larsen _et al._ , “Contracts for system design,” _Foundations and Trends® in Electronic Design Automation_ , vol. 12, no. 2-3, pp. 124–400, 2018.
  * [243] M. Fisher, L. A. Dennis, and M. P. Webster, “Verifying autonomous systems.” _Commun. ACM_ , vol. 56, no. 9, pp. 84–93, 2013.
  * [244] P. Čermák, A. Lomuscio, F. Mogavero, and A. Murano, “Mcmas-slk: A model checker for the verification of strategy logic specifications,” in _International Conference on Computer Aided Verification_. Springer, 2014, pp. 525–532.
  * [245] R. Fagin and J. Y. Halpern, “Belief, awareness, and limited reasoning,” _Artificial intelligence_ , vol. 34, no. 1, pp. 39–76, 1987.
  * [246] K. M. Sim, “Epistemic logic and logical omniscience: A survey,” _International Journal of Intelligent Systems_ , vol. 12, no. 1, pp. 57–81, 1997.