Using Formal Verification to Evaluate Human-Automation Interaction: A Review
---
paper_title: A model for types and levels of human interaction with automation

paper_content:

We outline a model for types and levels of automation that provides a framework and an objective basis for deciding which system functions should be automated and to what extent. Appropriate selection is important because automation does not merely supplant but changes human activity and can impose new coordination demands on the human operator. We propose that automation can be applied to four broad classes of functions: 1) information acquisition; 2) information analysis; 3) decision and action selection; and 4) action implementation. Within each of these types, automation can be applied across a continuum of levels from low to high, i.e., from fully manual to fully automatic. A particular system can involve automation of all four types at different levels. The human performance consequences of particular types and levels of automation constitute primary evaluative criteria for automation design using our model. Secondary evaluative criteria include automation reliability and the costs of decision/action consequences, among others. Examples of recommended types and levels of automation are provided to illustrate the application of the model to automation design.
---
paper_title: Human-Automation Interaction:

paper_content:

Automation does not mean humans are replaced; quite the opposite. Increasingly, humans are asked to interact with automation in complex and typically large-scale systems, including aircraft and air traffic control, nuclear power, manufacturing plants, military systems, homes, and hospitals. This is not an easy or error-free task for either the system designer or the human operator/automation supervisor, especially as computer technology becomes ever more sophisticated. This review outlines recent research and challenges in the area, including taxonomies and qualitative models of human-automation interaction; descriptions of automation-related accidents and studies of adaptive automation; and social, political, and ethical issues. Keywords: Driver distraction; Language: en
---
paper_title: PUMA Footprints: linking theory and craft skill in usability evaluation

paper_content:

‘Footprints’ are marks or features of a design that alert the analyst to the possible existence of ::: usability difficulties caused by violations of design principles. PUMA Footprints make an explicit link between ::: the theory underlying a Programmable User Model and the design principles that can be derived from that ::: theory. While principles are widely presented as being intuitively obvious, it is desirable that they should have a ::: theoretical basis. However, working directly with theory tends to be time-consuming, and demands a high level ::: of skill. PUMA footprints offer a theory-based justification for various usability principles, with guidelines on ::: detecting violations of those principles.
---
paper_title: Automated tool for task analysis of NextGen automation

paper_content:

The realization of NextGen capabilities will require rapid deployment of revised airline cockpit procedures and the pre-requisite training and proficiency checks. Traditional approaches for the evaluation of the re-designed procedures and training, such as expert reviews and human-in-the- loop tests, cannot provide comprehensive analysis, cannot be performed until after the procedures and training are developed, and are cost and time prohibitive. This paper describes the emergence of a new class of tools to automate the evaluation of procedures and training. The tools capture the procedures and tasks to be trained in a formal model that is stored in a data-base. Human performance models are executed to estimate the ease-of-learning, ease-of-use and likelihood of failure of each of the tasks. The procedures and tasks can be defined rapidly, and modified and run repeatedly throughout the development cycle. The underlying models and tools are described in this paper. A case study and the implications of these tools are also discussed.
---
paper_title: HOW IN THE WORLD DID WE EVER GET INTO THAT MODE? MODE ERROR AND AWARENESS IN SUPERVISORY CONTROL

paper_content:

New technology is flexible in the sense that it provides practitioners with a large number of functions and options for carrying out a given task under different circumstances. However, this flexibility has a price. Because the human supervisor must choose the mode best suited to a particular situation, he or she must know more than before about system operations and the operation of the system as well as satisfy new monitoring and attentional demands to track which mode the automation is in and what it is doing to manage the underlying processes. When designers proliferate modes without supporting these new cognitive demands, new mode-related error forms and failure paths can result. Mode error has been discussed in human-computer interaction for some time; however, the increased capabilities and the high level of autonomy of new automated systems appear to have created new types of mode-related problems. The authors explore these new aspects based on findings from their own and related studies of human-automation interaction. In particular, investigators draw on empirical data from a series of studies of pilot-automation interaction in commercial glass cockpit aircraft to illustrate the nature, circumstances, and potential consequences of mode awareness problems in supervisory control of automated resources. The result is an expanded view of mode error that considers the new demands imposed by more automated systems.
---
paper_title: Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors

paper_content:

Interactive systems combine a human operator with a computer. Either may be a source of error. The verification processes used must ensure both the correctness of the computer component, and also minimize the risk of human error. Human-centred design aims to do this by designing systems in a way that make allowance for human frailty. One approach to such design is to adhere to design rules. Design rules, however, are often ad hoc. We examine how a formal cognitive model, encapsulating results from the cognitive sciences, can be used to justify such design rules in a way that integrates their use with existing formal hardware verification techniques. We consider here the verification of a design rule intended to prevent a commonly occurring class of human error know as the post-completion error.
---
paper_title: ANALYSIS OF PILOTS' MONITORING AND PERFORMANCE ON AN AUTOMATED FLIGHT DECK

paper_content:

In order to understand the role of pilot monitoring in the loss of mode awareness on automated flight decks, we studied 20 Boeing 747-400 line pilots in a simulated flight. We developed a set of scenario events that created challenges to monitoring. We measured automation use, eye fixations, and pilot mental models. The results showed that, at an aggregate level, pilot monitoring patterns were consistent with those found in the few previous studies. However, mode awareness was affected by both failures to verify mode selections and an inability to understand the implications of autoflight mode on airplane performance.
---
paper_title: An Apprenticeship Approach for the Development of Operations Automation Knowledge Bases

paper_content:

Operations automation is automation that replaces, wholly or in part, operational activities currently carried out by human controllers in complex systems. It is intended to be neither ‘black-box’ nor ‘human-tended’ automation, but rather automation that functions independent of human control and yet still facilitates its inspection and repair as necessary. This paper describes research to develop an apprenticeship approach to developing a knowledge base to support such automation. The result is both a human-centered automation approach and a software architecture, Apprentice, to support this approach. Apprentice enables human operators to create the knowledge base for operations automation by performing their normal control activities. Apprentice watches and compares them with those specified in the knowledge base, noting discrepancies between the knowledge base and operator activities. Graphical knowledge base editing tools are then used—-by the domain practitioners—-to modify, refine, or extend the kno...
---
paper_title: On the representation of automation using a work domain analysis

paper_content:

Work domain analysis (WDA) has been applied extensively within cognitive engineering as an analytic framework for the evaluation of complex sociotechnical systems in support of design. However, the WDAs described in the literature have not explored the representation of automated system components, despite the documented problems associated with operator-automation interaction and the requirements for operator support in complex automated systems. The current research examines the application of WDA to model an example automated system – a camera – by representing the camera along with its automated components as separate systems using the abstraction hierarchy (AH). Additionally, we contrasted this modelling approach with the more typical approach of modelling automation within a cognitive work analysis (CWA) by performing a control task analysis using the decision ladder. The results of these analyses suggest that, similar to non-automated systems, considering a separate representation of an automated s...
---
paper_title: Humans and Automation: Use, Misuse, Disuse, Abuse

paper_content:

This paper addresses theoretical, empirical, and analytical studies pertaining to human use, misuse, disuse, and abuse of automation technology. Use refers to the voluntary activation or disengagement of automation by human operators. Trust, mental workload, and risk can influence automation use, but interactions between factors and large individual differences make prediction of automation use difficult. Misuse refers to over reliance on automation, which can result in failures of monitoring or decision biases. Factors affecting the monitoring of automation include workload, automation reliability and consistency, and the saliency of automation state indicators. Disuse, or the neglect or underutilization of automation, is commonly caused by alarms that activate falsely. This often occurs because the base rate of the condition to be detected is not considered in setting the trade-off between false alarms and omissions. Automation abuse, or the automation of functions by designers and implementation by man...
---
paper_title: A History and Primer of Human Performance Modeling

paper_content:

Human performance models are abstractions, usually mathematical or computational, that attempt to explain or predict human behavior in a particular domain or task. This includes a wide range of techniques and approaches, from ideas that are most likely familiar to the majority of human factors professionals (such as signal detection theory) to more novel and complex approaches (such as computational models of dual tasking while driving). This chapter provides a sampling of modeling approaches and domains to which those approaches have been applied; for a more in-depth review, see Pew and Mavor (1998). We also discuss some of the issues faced by modelers as well as describe some of the rich history of the modeling endeavor over the past 50 years. Language: en
---
paper_title: Ironies of Automation

paper_content:

Abstract This paper discusses the ways in which automation of industrial processes may expand rather than eliminate problems with the human operator. Some comments will be made on methods of alleviating these problems within the 'classic' approach of leaving the operator with responsibility for abnormal conditions, and on the potential for continued use of the human operator for on-line decision-making within human-computer collaboration.
---
paper_title: Human-Automated Judge Learning: A Methodology for Examining Human Interaction With Information Analysis Automation

paper_content:

Human-automated judge learning (HAJL) is a methodology providing a three-phase process, quantitative measures, and analytical methods to support design of information analysis automation. HAJL's measures capture the human and automation's judgment processes, relevant features of the environment, and the relationships between each. Specific measures include achievement of the human and the automation, conflict between them, compromise and adaptation by the human toward the automation, and the human's ability to predict the automation. HAJL's utility is demonstrated herein using a simplified air traffic conflict prediction task. HAJL was able to capture patterns of behavior within and across the three phases with measures of individual judgments and human-automation interaction. Its measures were also used for statistical tests of aggregate effects across human judges. Two between-subject manipulations were crossed to investigate HAJL's sensitivity to interventions in the human's training (sensor noise during training) and in display design (information from the automation about its judgment strategy). HAJL identified that the design intervention impacted conflict and compromise with the automation, participants learned from the automation over time, and those with higher individual judgment achievement were also better able to predict the automation.
---
paper_title: Integrating Task- and Work Domain-Based Work Analyses in Ecological Interface Design: A Process Control Case Study

paper_content:

In this paper, we present a case study wherein several work analysis methods were incorporated in the design of a graphical interface for a petrochemical production process. We follow this case from the application of the work analysis methods, through the consolidation of information requirements, to the design of a novel interface that integrates the requirements. The findings confirm earlier assertions that task-based and work domain-based analysis frameworks identify unique and complementary requirements for effective information systems that are intended to support supervisory control of complex systems. It further provides the first industrial demonstration of ecological interface forms based on integrated task-and work domain-based work requirements.
---
paper_title: Brittleness in the design of cooperative problem-solving systems: the effects on user performance

paper_content:

One of the critical problems in the design and use of advanced decision-support systems is their potential "brittleness". This brittleness can arise because of the inability of the designer to anticipate and design for all of the scenarios that could arise during the use of the system. The typical "safety valve" to deal with this problem is to keep a person "in the loop", requiring that person to apply his/her expertise in making the final decision on what actions to take. This paper provides empirical data on how the role of the decision support system can have a major impact on the effectiveness of this design strategy. Using flight planning for commercial airlines as a testbed, three alternative designs for a graphical flight planning tool were evaluated, using 27 dispatchers and 30 pilots as subjects. The results show that the presentation of a suggestion or recommendation by the computer early in the person's own problem evaluation can have a significant impact on that person's decision processes, influencing situation assessment and the evaluation of alternative solutions.
---
paper_title: Flight deck automation and task management

paper_content:

The purpose of the paper is to show that recent flight deck automation human factors research suggests that attention allocation or task management is a critical safety issue in advanced technology aircraft, to relate that finding to task management research, and to suggest a course for future research to address that issue.
---
paper_title: Using multiple cognitive task analysis methods for supervisory control interface design in high-throughput biological screening processes

paper_content:

Cognitive task analysis (CTA) approaches are currently needed in many domains to provide explicit guidance on redesigning existing systems. This study used goal-directed task analysis (GDTA) along with abstraction hierarchy (AH) modeling to characterize the knowledge structure of biopharmacologists in planning, executing and analyzing the results of high-throughput organic compound screening operations, as well as the lab automation and equipment used in these operations. It was hypothesized that combining the results of the GDTA and AH models would provide a better understanding of complex system operator needs and how they may be addressed by existing technologies, as well as facilitate identification of automation and system interface design limitations. We used comparisons of the GDTA and AH models along with taxonomies of usability heuristics and types of automation in order to formulate interface design and automation functionality recommendations for existing software applications used in biological screening experiments. The proposed methodology yielded useful recommendations for improving custom supervisory control applications that led to prototypes of interface redesigns. The approach was validated through an expert usability evaluation of the redesigns and was shown to be applicable to the life sciences domain.
---
paper_title: Using GOMS for user interface design and evaluation: which technique?

paper_content:

Since the seminal book, The Psychology of Human-Computer Interaction , the GOMS model has been one of the few widely known theoretical concepts in human-computer interaction. This concept has spawned much research to verify and extend the original work and has been used in real-world design and evaluation situations. This article synthesizes the previous work on GOMS to provide an integrated view of GOMS models and how they can be used in design. We briefly describe the major variants of GOMS that have matured sufficiently to be used in actual design. We then provide guidance to practitioners about which GOMS variant to use for different design situations. Finally, we present examples of the application of GOMS to practical design problems and then summarize the lessons learned.
---
paper_title: Human-Automation Interaction:

paper_content:

Automation does not mean humans are replaced; quite the opposite. Increasingly, humans are asked to interact with automation in complex and typically large-scale systems, including aircraft and air traffic control, nuclear power, manufacturing plants, military systems, homes, and hospitals. This is not an easy or error-free task for either the system designer or the human operator/automation supervisor, especially as computer technology becomes ever more sophisticated. This review outlines recent research and challenges in the area, including taxonomies and qualitative models of human-automation interaction; descriptions of automation-related accidents and studies of adaptive automation; and social, political, and ethical issues. Keywords: Driver distraction; Language: en
---
paper_title: Spatial Awareness in Synthetic Vision Systems: Using Spatial and Temporal Judgments to Evaluate Texture and Field of View

paper_content:

OBJECTIVE ::: This work introduced judgment-based measures of spatial awareness and used them to evaluate terrain textures and fields of view (FOVs) in synthetic vision system (SVS) displays. ::: ::: ::: BACKGROUND ::: SVSs are cockpit technologies that depict computer-generated views of terrain surrounding an aircraft. In the assessment of textures and FOVs for SVSs, no studies have directly measured the three levels of spatial awareness with respect to terrain: identification of terrain, its relative spatial location, and its relative temporal location. ::: ::: ::: METHODS ::: Eighteen pilots made four judgments (relative azimuth angle, distance, height, and abeam time) regarding the location of terrain points displayed in 112 noninteractive 5-s simulations of an SVS head-down display. There were two between-subject variables (texture order and FOV order) and five within-subject variables (texture, FOV, and the terrain point's relative azimuth angle, distance, and height). ::: ::: ::: RESULTS ::: Texture produced significant main and interaction effects for the magnitude of error in the relative angle, distance, height, and abeam time judgments. FOV interaction effects were significant for the directional magnitude of error in the relative distance, height, and abeam time judgments. ::: ::: ::: CONCLUSION ::: Spatial awareness was best facilitated by the elevation fishnet (EF), photo fishnet (PF), and photo elevation fishnet (PEF) textures. ::: ::: ::: APPLICATION ::: This study supports the recommendation that the EF, PF, and PEF textures be further evaluated in future SVS experiments. Additionally, the judgment-based spatial awareness measures used in this experiment could be used to evaluate other display parameters and depth cues in SVSs.
---
paper_title: Interactive Critiquing as a Form of Decision Support: An Empirical Evaluation

paper_content:

This research focused on the design of a decision-support system to assist blood bankers in identifying alloantibodies in patients' blood. It was hypothesized that critiquing, a technique in which a computer monitors human performance for errors, would be an effective role for such a decision-support system if the error monitoring was unobtrusive and if the critiquing was in response to both intermediate and final conclusions made by the user. A prototype critiquing system monitored medical technologists for (a) errors of commission and errors of omission, b) failure to follow a complete protocol, (c) answers inconsistent with the data collected, and (d) answers inconsistent with prior probability information. Participants using the critiquing system had significantly better performance (completely eliminating misdiagnosis rates for 3 out of 4 test cases) than a comparable control group. Detailed analysis of the behavioral protocols provided insights into how specific design features influenced performanc...
---
paper_title: Designing Effective Human-Automation-Plant Interfaces: A Control-Theoretic Perspective

paper_content:

In this article, we propose the application of a control-theoretic framework to human-automation interaction. The framework consists of a set of conceptual distinctions that should be respected in automation research and design. We demonstrate how existing automation interface designs in some nuclear plants fail to recognize these distinctions. We further show the value of the approach by applying it to modes of automation. The design guidelines that have been proposed in the automation literature are evaluated from the perspective of the framework. This comparison shows that the framework reveals insights that are frequently overlooked in this literature. A new set of design guidelines is introduced that builds upon the contributions of previous research and draws complementary insights from the control-theoretic framework. The result is a coherent and systematic approach to the design of human-automation-plant interfaces that will yield more concrete design criteria and a broader set of design tools. Applications of this research include improving the effectiveness of human-automation interaction design and the relevance of human-automation interaction research.
---
paper_title: A specifier's introduction to formal methods

paper_content:

Formal methods used in developing computer systems (i.e. mathematically based techniques for describing system properties) are defined, and their role is delineated. Formal specification languages, which provide the formal method's mathematical basis, are examined. Certain pragmatic concerns about formal methods and their users, uses, and characteristics are discussed. Six well-known or commonly used formal methods are illustrated by simple examples. They are Z, VDM, Larch, temporal logic, CSP, and transition axioms. >
---
paper_title: An improvement in formal verification

paper_content:

Critical safety and liveness properties of a concurrent system can often be proven with the help of a reachability analysis of a finite state model. This type of analysis is usually implemented as a depthfirst search of the product statespace of all components in the system, with each (finite state) component modeling the behavior of one asynchronously executing process. Formal verification is achieved by coupling the depthfirst search with a method for identifying those states or sequences of states that violate the correct- ness requirements. It is well known, however, that an exhaustive depthfirst search of this type performs redundant work. The redundancy is caused by the many possible interleavings of inde- pendent actions in a concurrent system. Few of these interleavings can alter the truth or falsity of the correctness properties being studied. The standard depthfirst search algorithm can be modified to track additional information about the interleavings that have already been inspected, and use this information to avoid the exploration of redundant interleavings. Care must be taken to perform the reductions in such a way that the capability to prove both safety and liveness properties is fully pre- served. Not all known methods have this property. Another potential drawback of the existing methods is that the additional computations required to enforce a reduction dur- ing the search can introduce overhead that diminishes the benefits. In this paper we dis- cuss a new reduction method that solves some of these problems.
---
paper_title: A machine program for theorem-proving

paper_content:

The programming of a proof procedure is discussed in connection with trial runs and possible improvements.
---
paper_title: Counterexample-guided abstraction refinement for symbolic model checking

paper_content:

The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.
---
paper_title: Verifying Invariants Using theorem Proving

paper_content:

Our goal is to use a theorem prover in order to verify invariance properties of distributed systems in a “model checking like” manner. A system S is described by a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of S, we try to compute, in a model checking like manner, the weakest predicate P′ stronger than P and weaker than Init which is an inductive invariant, that is, whenever P′ is true in some state, then P′ remains true after the execution of any possible transition. The fact that P is an invariant can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove these predicates, we use either automatic or assisted theorem proving depending on their nature.
---
paper_title: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

paper_content:

A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe {(+), (-), (±)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, …).
---
paper_title: Physigrams: modelling devices for natural interaction

paper_content:

This paper explores the formal specification of the physical behaviour of devices ‘unplugged’ from their digital effects. By doing this we seek to better understand the nature of physical interaction and the way this can be exploited to improve the design of hybrid devices with both physical and digital features. We use modified state transition networks of the physical behaviour, which we call physiograms, and link these to parallel diagrams of the digital state. These are used to describe a number of features of physical interaction exposed by previous work and relevant properties expressed using a formal semantics of the diagrams. As well as being an analytic tool, the physigrams have been used in a case study where product designers used and adapted them as part of the design process.
---
paper_title: A Review of Formalisms for Describing Interactive Behaviour

paper_content:

This paper reviews the state of research linking formal specification and interactive systems. An appreciation of Human Computer Interaction has become increasingly important within Software Engineering. As systems have become more complex there is an increasing awareness of the consequences of human error. As a result the formal specification of interactive behaviour has become a pressing topic of research. The notations considered here describe both the capabilities and resources of users in relation to a specific system and those aspects of an interactive system that must be analysed from a user perspective before implementation. The review concludes by surveying ongoing work which attempts to bridge the gap between disciplinary standpoints.
---
paper_title: Formal verification of humanautomation interaction

paper_content:

This paper discusses a formal and rigorous approach to the analysis of operator interaction with machines. It addresses the acute problem of detecting design errors in human-machine interaction and focuses on verifying the correctness of the interaction in complex and automated control systems. The paper describes a systematic methodology for evaluating whether the interface provides the necessary information about the machine to enable the operator to perform a specified task successfully and unambiguously. It also addresses the adequacy of information provided to the user via training material (e.g., user manual) about the machine's behavior. The essentials of the methodology, which can be automated and applied to the verification of large systems, are illustrated by several examples and through a case study of pilot interaction with an autopilot aboard a modern commercial aircraft. The expected application of this methodology is an augmentation and enhancement, by formal verification, of human-automation interfaces.
---
paper_title: On the use of transition diagrams in the design of a user interface for an interactive computer system

paper_content:

This paper deals with what might be called the top level design of an interactive computer system. It examines some problems which arise in trying to specify what the user interface of such a system should be. It proposes a concept—the terminal state—and a notation—the terminal state transition diagram—which make the design of the top level somewhat easier. It also proposes a user interface in which the notion of terminal state is explicit. This user interface seems to provide a great improvement in flexibility and case of adding subsystems to a general purpose system.
---
paper_title: Press on: Principles of Interaction Programming

paper_content:

Choice Outstanding Academic Title, 2008. and Winner, Computer and Information Sciences category, 2007 Professional/Scholarly Publishing Awards for Excellence Competition presented by the Association of American Publishers, Inc. Interactive systems and devices, from mobile phones to office copiers, do not fulfill their potential for a wide variety of reasonsnot all of them technical. Press On shows that we can design better interactive systems and devices if we draw on sound computer science principles. It uses state machines and graph theory as a powerful and insightful way to analyze and design better interfaces and examines specific designs and creative solutions to design problems. Programmerswho have the technical knowledge that designers and users often lackcan be more creative and more central to interaction design than we might think. Sound programming concepts improve device design. Press On provides the insights, concepts and programming tools to improve usability. Knowing the computer science is fundamental, but Press On also shows how essential it is to have the right approaches to manage the design of systems that people use. Particularly for complex systems, the social, psychological and ethical concernsthe wider design issuesare crucial, and these are covered in depth. Press On highlights key principles throughout the text and provides cross-topic linkages between chapters and suggestions for further reading. Additional material, including all the program code used in the book, is available on an interactive web site. Press On is an essential textbook and reference for computer science students, programmers, and anyone interested in the design of interactive technologies.
---
paper_title: Analyzing interaction orderings with model checking

paper_content:

Human-computer interaction (HCI) systems control an ongoing interaction between end-users and computer-based systems. For software-intensive systems, a graphic user interface (GUI) is often employed for enhanced usability. Traditional approaches to validation of GUI aspects in HCI systems involve prototyping and live-subject testing. These approaches are limited in their ability to cover the set of possible human-computer interactions that a system may allow, since patterns of interaction may be long running and have large numbers of alternatives. In this paper, we propose a static analysis that is capable of reasoning about user-interaction properties of GUI portions of HCI applications written in Java using modern GUI frameworks, such as Swing/spl trade/. Our approach consists of partitioning an HCI application into three parts: the Swing library, the GUI implementation, i.e., code that interacts directly with Swing, and the underlying application. We develop models of each of these parts that preserve behavior relevant to interaction ordering. We describe how these models are generated and how we have customized a model checking framework to efficiently analyze their combination.
---
paper_title: Model checking graphical user interfaces using abstractions

paper_content:

Symbolic model checking techniques have been widely and successfully applied to statically analyze dynamic properties of hardware systems. Efforts to apply this same technology to the analysis of software systems has met with a number of obstacles, such as the existence of non-finite state-spaces. This paper investigates abstractions that make it possible to cost-effectively model check specifications of software for graphical user interface (GUI) systems. We identify useful abstractions for this domain and demonstrate that they can be incorporated into the analysis of a variety of systems with similar structural characteristics. The resulting domain-specific model checking yields fast verification of naturally occur ring specifications of intended GUI behavior.
---
paper_title: A Formalism for the Specification of Operationally Embedded Reactive Systems

paper_content:

The Operational Procedure Information Model, presented in this paper, provides a formalism for the specification of the behavior of operationally embedded reactive systems found in aircraft guidance and navigation systems. The information model assigns semantic interpretations of the operational procedure construct to the elements of a finite state machine. The operational procedure construct captures the embedded operational behavior of the system over all the missions in the life-cycle. The finite state machine captures the reactive behavior of the system. ::: ::: ::: ::: The information model, captured in a database and interrogated through a graphical user-interface, can be used for simulation, analysis, and the generation of code and documentation.
---
paper_title: A formal model to handle the adaptability of multimodal user interfaces

paper_content:

In this paper we propose an approach for checking adaptability property of multimodal User Interfaces (UIs) for systems used in dynamic environments like mobile phones and PDAs. The approach is based on a formal description of both the multimodal interaction and the property. The SMV model-checking formal technique is used for the verification process of the property. The approach is defined in two steps. First, the system is described using a formal model, and the property is specified using CTL (Computation Tree Logic) temporal logic. Then, we assume that an environment changes such that at most one modality of the system is disabled. For this propose, Disable is defined as a formal operator that disables a modality in the system. The property is checked by using the SMV (Symbolic Model Verifier) model-checker on all systems resulting from desabling a modality of the system. The approach reduces the complexity of the model-checking process and allows the verification at earlier stages of the development life cycle. We apply this approach on a mobile phone case study.
---
paper_title: Formal Reasoning about Dialogue Properties with Automatic Support

paper_content:

Abstract One of the advantages of using formal methods in the design of human–computer interfaces is the possibility to reason about user interface properties. Model checking techniques provide a useful support to this end. This paper discusses the possibilities of verifying the properties of user interfaces and related problems, such as when the dialogue specification has an infinite number of states. We provide an example of a set of general user interfaces properties, and we show how these properties can be tailored for specific cases and thus be used as a framework to evaluate the design of the interactive application considered.
---
paper_title: Formally verifying interactive systems: A review

paper_content:

Although some progress has been made in the development of principles to guide the designers of interactive systems, ultimately the only proven method of checking how usable a particular system is must be based on experiment. However, it is also the case that changes that occur at this late stage are very expensive. The need for early design checking increases as software becomes more complex and is designed to serve volume international markets and also as interactions between operators and automation in safety-critical environments becomes more complex. This paper reviews progress in the area of formal verification of interactive systems and proposes a short agenda for further work.
---
paper_title: Systematic Analysis of Control Panel Interfaces Using Formal Tools

paper_content:

The paper explores the role that formal modeling may play in aiding the visualization and implementation of usability requirements of a control panel. We propose that this form of analysis should become a systematic and routine aspect of the development of such interfaces. We use a notation for describing the interface that is convenient to use by software engineers, and describe a set of tools designed to make the process systematic and exhaustive.
---
paper_title: Validating Human-device Interfaces with Model Checking and Temporal Logic Properties Automatically Generated from Task Analytic Models

paper_content:

When evaluating designs of human-device interfaces for safety critical systems, it is very important that they be valid: support the goal-directed tasks they were designed to facilitate. Model checking is a type of formal analysis that is used to mathematically prove whether or not a model of a system does or does not satisfy a set of specification properties, usually written in a temporal logic. In the analysis of human-automation interaction, model checkers have been used to formally verify that human-device interface models are valid with respect to goal-directed tasks encoded in temporal logic properties. All of the previous work in this area has required that analysts manually specify these properties. Given the semantics of temporal logic and the complexity of task analytic behavior models, this can be very difficult. This paper describes a method that allows temporal logic properties to be automatically generated from task analytic models created early in the system design process. This allows analysts to use model checkers to validate that modeled human-device interfaces will allow human operators to successfully perform the necessary tasks with the system. The use of the method is illustrated with a patient controlled analgesia pump programming example. The method is discussed and avenues for future work are described.
---
paper_title: An integrated framework for the analysis of dependable interactive systems (IFADIS): Its tool support and evaluation

paper_content:

This paper discusses a method for the analysis of dependable interactive systems using model checking, and its support by a tool designed to make it accessible to a broader community. The method and the tool are designed to be of value to system engineers, usability engineers and software engineers. It has been designed to help usability engineers by making those aspects of the analysis relevant to them explicit while concealing those aspects of modelling and model checking that are not relevant. The paper presents the results of a user evaluation of the effectiveness of aspects of the tool and how it supports the proposed method.
---
paper_title: Analyzing interaction orderings with model checking

paper_content:

Human-computer interaction (HCI) systems control an ongoing interaction between end-users and computer-based systems. For software-intensive systems, a graphic user interface (GUI) is often employed for enhanced usability. Traditional approaches to validation of GUI aspects in HCI systems involve prototyping and live-subject testing. These approaches are limited in their ability to cover the set of possible human-computer interactions that a system may allow, since patterns of interaction may be long running and have large numbers of alternatives. In this paper, we propose a static analysis that is capable of reasoning about user-interaction properties of GUI portions of HCI applications written in Java using modern GUI frameworks, such as Swing/spl trade/. Our approach consists of partitioning an HCI application into three parts: the Swing library, the GUI implementation, i.e., code that interacts directly with Swing, and the underlying application. We develop models of each of these parts that preserve behavior relevant to interaction ordering. We describe how these models are generated and how we have customized a model checking framework to efficiently analyze their combination.
---
paper_title: Model checking graphical user interfaces using abstractions

paper_content:

Symbolic model checking techniques have been widely and successfully applied to statically analyze dynamic properties of hardware systems. Efforts to apply this same technology to the analysis of software systems has met with a number of obstacles, such as the existence of non-finite state-spaces. This paper investigates abstractions that make it possible to cost-effectively model check specifications of software for graphical user interface (GUI) systems. We identify useful abstractions for this domain and demonstrate that they can be incorporated into the analysis of a variety of systems with similar structural characteristics. The resulting domain-specific model checking yields fast verification of naturally occur ring specifications of intended GUI behavior.
---
paper_title: Automatic detection of interaction vulnerabilities in an executable specification

paper_content:

This paper presents an approach to providing designers with the means to detect Human-Computer Interaction (HCI) vulnerabilities without requiring extensive HCI expertise. The goal of the approach is to provide timely, useful analysis results early in the design process, when modifications are less expensive. The twin challenges of providing timely and useful analysis results led to the development and evaluation of computational analyses, integrated into a software prototyping toolset. The toolset, referred to as the Automation Design and Evaluation Prototyping Toolset (ADEPT) was constructed to enable the rapid development of an executable specification for automation behavior and user interaction. The term executable specification refers to the concept of a testable prototype whose purpose is to support development of a more accurate and complete requirements specification.
---
paper_title: HMI aspects of automotive climate control systems

paper_content:

In this paper we discuss a formal approach to the design and analysis of automotive systems, from a human-machine interaction (HMI) point of view. Specifically, we detail the behavior of a generic climate control system, present a statecharts model of this system, and discuss aspects of user interaction analysis. Several general principles for the design of climate control systems are illustrated and discussed. The topic of design patterns, in the context of a formal description of user interaction, is introduced, and two design patterns are illustrated and discussed.
---
paper_title: Interaction engineering using the IVY tool

paper_content:

This paper is concerned with support for the process of usability engineering. The aim is to use formal techniques to provide a systematic approach that is more traceable, and because it is systematic, repeatable. As a result of this systematic process some of the more subjective aspects of the analysis can be removed. The technique explores exhaustively those features of a specific design that fail to satisfy a set of properties. It also analyzes those aspects of the design where it is possible to quantify the cost of use. The method is illustrated using the example of a medical device. While many aspects of the approach and its tool support have already been discussed elsewhere, this paper builds on and contrasts an analysis of the same device provided by a third party and in so doing enhances the IVY tool.
---
paper_title: NUSMV: a new Symbolic Model Verifier

paper_content:

This paper describes NUSMV, a new symbolic model checker developed as a joint project between Carnegie Mellon University (CMU) and Istituto per la Ricerca Scientifica e Tecnolgica (IRST). NUSMV is designed to be a well structured, open, flexible and documented platform for model checking. In order to make NUSMV applicable in technology transfer projects, it was designed to be very robust, close to the standards required by industry, and to allow for expressive specification languages. NUSMV is the result of the reengineering, reimplementation and extension of SMV [6], version 2.4.4 (SMV from now on). With respect to SMV, NUSMV has been extended and upgraded along three dimensions. First, from the point of view of the system functionalities, NUSMV features a textual interaction shell and a graphical interface, extended model partitioning techniques, and allows for LTL model checking. Second, the system architecture of NUSMV has been designed to be highly modular and open. The interdependencies between different modules have been separated, and an external, state of the art BDD package [8] has been integrated in the system kernel. Third, the quality of the implementation has been strongly enhanced. This makes of NUSMV a robust, maintainable and well documented system, with a relatively easy to modify source code. NUSMV is available at http://nusmv.irst.itc.it/.
---
paper_title: Communicating sequential processes

paper_content:

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar programming exercises.
---
paper_title: A formal methods approach to the analysis of mode confusion

paper_content:

The goal of the new NASA Aviation Safety Program (AvSP) is to reduce the civil aviation fatal accident rate by 80% in ten years and 90% in twenty years. This program is being driven by the accident data with a focus on the most recent history. Pilot error is the most commonly cited cause for fatal accidents (up to 70%) and obviously must be given major consideration in this program. While the greatest source of pilot error is the loss of situation awareness, mode confusion is increasingly becoming a major contributor as well. This paper will explore how formal models and analyses can be used to help eliminate mode confusion from flight deck designs and at the same time increase our confidence in the safety of the implementation. The paper is based upon interim results from a new project involving NASA Langley and Rockwell Collins in applying formal methods to a realistic business jet Flight Guidance System (FGS).
---
paper_title: A Rigorous View of Mode Confusion

paper_content:

Not only in aviation psychology, mode confusion is recognised as a significant safety concern. The notion is used intuitively in the pertinent literature, but with surprisingly different meanings. We present a rigorous way of modelling the human and the machine in a shared-control system. This enables us to propose a precise definition of mode and mode confusion. In our modelling approach, we extend the commonly used distinction between the machine and the user's mental model of it by explicitly separating these and their safety-relevant ions. Furthermore, we show that distinguishing three different interfaces during the design phase reduces the potential for mode confusion. A result is a new classification of mode confusions by cause, leading to a number of design recommendations for shared-control systems which help to avoid mode confusion problems. A further result is a foundation for detecting mode confusion problems by model checking.
---
paper_title: Safety-relevant mode confusions – modelling and reducing them

paper_content:

Abstract Mode confusions are a significant safety concern in safety-critical systems, for example in aircraft. A mode confusion occurs when the observed behaviour of a technical system is out of sync with the user's mental model of its behaviour. But the notion is described only informally in the literature. We present a rigorous way of modelling the user and the machine in a shared-control system. This enables us to propose precise definitions of ‘mode’ and ‘mode confusion’ for safety-critical systems. We then validate these definitions against the informal notions in the literature. A new classification of mode confusions by cause leads to a number of design recommendations for shared-control systems. These help in avoiding mode confusion problems. Our approach supports the automated detection of remaining mode confusion problems. We apply our approach practically to a wheelchair robot.
---
paper_title: Formal verification of humanautomation interaction

paper_content:

This paper discusses a formal and rigorous approach to the analysis of operator interaction with machines. It addresses the acute problem of detecting design errors in human-machine interaction and focuses on verifying the correctness of the interaction in complex and automated control systems. The paper describes a systematic methodology for evaluating whether the interface provides the necessary information about the machine to enable the operator to perform a specified task successfully and unambiguously. It also addresses the adequacy of information provided to the user via training material (e.g., user manual) about the machine's behavior. The essentials of the methodology, which can be automated and applied to the verification of large systems, are illustrated by several examples and through a case study of pilot interaction with an autopilot aboard a modern commercial aircraft. The expected application of this methodology is an augmentation and enhancement, by formal verification, of human-automation interfaces.
---
paper_title: Hybrid verification of an interface for an automatic landing

paper_content:

Modern commercial aircraft have extensive automation which helps the pilot by performing computations, obtaining data, and completing procedural tasks. The pilot display must contain enough information so that the pilot can correctly predict the aircraft's behavior, while not overloading the pilot with unnecessary information. Human-automation interaction is currently evaluated through extensive simulation. In this paper, using both hybrid and discrete-event system techniques, we show how one could mathematically verify that an interface contains enough information for the pilot to safely and unambiguously complete a desired maneuver. We first develop a nonlinear, hybrid model for the longitudinal dynamics of a large civil jet aircraft in an autoland/go-around maneuver. We find the largest controlled subset of the aircraft's flight envelope for which we can guarantee both safe landing and safe go-around. We abstract a discrete procedural model using this result, and verify a discrete formulation of the pilot display against it. An interface which fails this verification could result in nondeterministic or unpredictable behavior from the pilot's point of view.
---
paper_title: A bisimulation-based approach to the analysis of human-computer interaction

paper_content:

This paper discusses the use of formal methods for analysing human-computer interaction. We focus on the mode confusion problem that arises whenever the user thinks that the system is doing something while it is in fact doing another thing. We consider two kinds of models: the system model describes the actual behaviour of the system and the mental model represents the user's knowledge of the system. The user interface is modelled as a subset of system transitions that the user can control or observe. We formalize a full-control property which holds when a mental model and associated user interface are complete enough to allow proper control of the system. This property can be verified using model-checking techniques on the parallel composition of the two models. We propose a bisimulation-based equivalence relation on the states of the system and show that, if the system satisfies a determinism condition with respect to that equivalence, then minimization modulo that equivalence produces a minimal mental model that allows full-control of the system. We enrich our approach to take operating modes into account. We give experimental results obtained by applying a prototype implementation of the proposed techniques to a simple model of an air-conditioner.
---
paper_title: A method for predicting errors when interacting with finite state systems. How implicit learning shapes the user's knowledge of a system

paper_content:

Abstract This paper describes a method for predicting the errors that may appear when human operators or users interact with systems behaving as finite state systems. The method is a generalization of a method used for predicting errors when interacting with autopilot modes on modern, highly computerized airliners [Proc 17th Digital Avionics Sys Conf (DASC) (1998); Proc 10th Int Symp Aviat Psychol (1999)]. A cognitive model based on spreading activation networks is used for predicting the user's model of the system and its impact on the production of errors. The model strongly posits the importance of implicit learning in user–system interaction and its possible detrimental influence on users' knowledge of the system. An experiment conducted with Airbus Industrie and a major European airline on pilots' knowledge of autopilot behavior on the A340-200/300 confirms the model predictions, and in particular the impact of the frequencies with which specific state transitions and contexts are experienced.
---
paper_title: Models and Mechanized Methods that Integrate Human Factors into Automation Design

paper_content:

Recent work h as s hown a c onvergence between the Human Factors and Formal Methods communities that opens promising n ew directions for collaborative work in calculating, predicting, and analyzing the behavior of complex aeronautical systems and their operators. Previously it has been shown that fully automatic, finitestate verification techniques can be used to identify likely sources of mode c onfusion in existing systems; i n this paper we focus on use of these techniques in the design of new systems. We use a simple e xample to d emonstrate how automated finite-state techniques can be used to explore autopilot design options, and then suggest additional applications for this technique, including the validation of empirically-derived, minimal mental models of autopilot behavior.
---
paper_title: On Preventing Telephony Feature Interactions which are Shared-Control Mode Confusions

paper_content:

We demonstrate that many undesired telephony feature interactions are also shared-control mode confusions. A mode confusion occurs when the observed behaviour of a technical system is out of sync with the behaviour of the user’s mental model of it. Several measures for preventing mode confusions are known in the literature on human-computer interaction. We show that these measures can be applied to this kind of feature interaction. We sketch several more measures for the telephony domain.
---
paper_title: Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises

paper_content:

Abstract Automation surprises occur when an automated system behaves differently than its operator expects. If the actual system behavior and the operator's ‘mental model’ are both described as finite state transition systems, then mechanized techniques known as ‘model checking’ can be used automatically to discover any scenarios that cause the behaviors of the two descriptions to diverge from one another. These scenarios identify potential surprises and pinpoint areas where design changes, or revisions to training materials or procedures, should be considered. The mental models can be suggested by human factors experts, or can be derived from training materials, or can express simple requirements for ‘consistent’ behavior. The approach is demonstrated by applying the Muro state exploration system to a ‘kill-the-capture’ surprise in the MD-88 autopilot. This approach does not supplant the contributions of those working in human factors and aviation psychology, but rather provides them with a tool to examine properties of their models using mechanized calculation. These calculations can be used to explore the consequences of alternative designs and cues, and of systematic operator error, and to assess the cognitive complexity of designs. The description of model checking is tutorial and is hoped to be accessible to those from the human factors community to whom this technology may be new.
---
paper_title: The Role of Working Memory on Measuring Mental Models of Physical Systems

paper_content:

Up until now there has been no agreement on what a mental model of a physical system is and how to infer the mental model a person has. This paper describes research aimed at solving these problems by proposing that a Mental Model is a dynamic representation created in WM by combining information stored in LTM (the Conceptual Model of the system) and characteristics extracted from the environment. Three experiments tested hypotheses derived from this proposal. Implications for research on Mental Model are discussed.
---
paper_title: A formal framework for design and analysis of human-machine interaction

paper_content:

Automated systems are increasingly complex, making it hard to design interfaces for human operators. Human-machine interaction (HMI) errors like automation surprises are more likely to appear and lead to system failures or accidents. In previous work, we studied the problem of generating system abstractions, called mental models, that facilitate system understanding while allowing proper control of the system by operators as defined by the full-control property. Both the domain and its mental model have Labelled Transition Systems (LTS) semantics, and we proposed algorithms for automatically generating minimal mental models as well as checking full-control. This paper presents a methodology and an associated framework for using the above and other formal method based algorithms to support the design of HMI systems. The framework can be used for modelling HMI systems and analysing models against HMI vulnerabilities. The analysis can be used for validation purposes or for generating artifacts such as mental models, manuals and recovery procedures. The framework is implemented in the JavaPathfinder model checker. Our methodology is demonstrated on two examples, an existing benchmark of a medical device, and a model generated from the ADEPT toolset developed at NASA Ames. Guidelines about how ADEPT models can be translated automatically into JavaPathfinder models are also discussed.
---
paper_title: Protocol Verification as a Hardware Design Aid

paper_content:

The role of automatic formal protocol verification in hardware design is considered. Principles that maximize the benefits of protocol verification while minimizing the labor and computation required are identified. A novel protocol description language and verifier (both called Mur phi ) are described, along with experiences in applying them to two industrial protocols that were developed as part of hardware designs. >
---
paper_title: Immediate observability of discrete event systems with application to user-interface design

paper_content:

A human interacting with a hybrid system is often presented, through information displays, with a simplified representation of the underlying system. This interface should not overwhelm the human with unnecessary information, and thus usually contains only a subset of information about the true system model, yet, if properly designed, represents an abstraction of the true system which the human is able to use to safely interact with the system [M. Heymann and A. Degani, 2002]. For cases in which the human interacts with all or part of the system from a remote location, and communication has a high cost, the need for a simple abstraction, which reduces the amount of information that must be transmitted, is of the utmost importance. The user should be able to immediately determine the actual state of the system, based on the information displayed through the interface. In this paper, we derive conditions for immediate observability in which the current state of the system can be unambiguously reconstructed from the output associated with the current state and the last or next event. Then, we show how to construct a discrete event system output function, which makes a system immediately observable, and apply this to a reduced state machine, which represents an interface.
---
paper_title: An automated method to detect potential mode confusions

paper_content:

Mode confusions are a type of "automation surprise"-circumstances where an automated system behaves differently than its operator expects. It is generally accepted that operators develop "mental models" for the behavior of automated systems and use these to guide their interaction with the systems concerned, so that an automation surprise results when the actual system behavior diverges from its operator's mental model. Complex systems are often structured into "modes" (for example, an autopilot might have different modes for altitude capture, altitude hold, and so on), and their behavior can change significantly across different modes. "Mode confusion" arises when the system is in a different mode than that assumed by its operator; this is a rich source of automation surprises, since the operator may interact with the system according to a mental model that is inappropriate for its actual mode. Mode confusions have been implicated in several recent crashes and other incidents, and are a growing source of concern in modern automated cockpits. If we accept that mode confusions are due to a mismatch between the actual behavior of a system and the mental model of its operator, then one way to look for potential mode confusions is to compare the design of the actual system against a mental model. There are two challenges here: how to get hold of a mental model, and how to do the comparison. Through observation, questionnaires, and other techniques, psychologists have been able to elicit the mental models of individual operators (typically pilots). However, comparison between a design and the mental model of a specific individual will provide only very specific information; we are interested in whether a design is prone to mode confusions, and for this purpose it is more useful to compare the design against a generic mental model rather than that of an individual.
---
paper_title: Formal Modeling and Analysis for Interactive Hybrid Systems

paper_content:

An effective strategy for discovering certain kinds of automation surprise and other problems in interactive systems is to build models of the participating (automated and human) agents and then explore all reachable states of the composed system looking for divergences between mental states and those of the automation. Various kinds of model checking provide ways to automate this approach when the agents can be modeled as discrete automata. But when some of the agents are continuous dynamical systems (e.g., airplanes), the composed model is a hybrid (i.e., mixed continuous and discrete) system and these are notoriously hard to analyze. We describe an approach for very abstract modeling of hybrid systems using rela- tional approximations and their automated analysis using infinite bounded model checking supported by an SMT solver. When counterexamples are found, we de- scribe how additional constraints can be supplied to direct counterexamples toward plausible scenarios that can be confirmed in high-fidelity simulation. The approach is illustrated though application to a known (and now corrected) human-automation interaction problem in Airbus aircraft.
---
paper_title: Formal Models for Cooperative Tasks: Concepts and an Application for En-Route Air-Traffic Control

paper_content:

This paper presents a proposal for specifying task models for cooperative applications that allow designers to describe the relationships between the activities performed by various users involved in cooperative environments. To this end we extend the ConcurTaskTree notation so that new information useful for describing complex cooperative applications can be clearly specified. An example of application to describe En-Route Air Traffic Control (ATC) is given to illustrate and clarify our approach.
---
paper_title: Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking

paper_content:

Breakdowns in complex systems often occur as a result of system elements interacting in unanticipated ways. In systems with human operators, human-automation interaction associated with both normative and erroneous human behavior can contribute to such failures. Model-driven design and analysis techniques provide engineers with formal methods tools and techniques capable of evaluating how human behavior can contribute to system failures. This paper presents a novel method for automatically generating task analytic models encompassing both normative and erroneous human behavior from normative task models. The generated erroneous behavior is capable of replicating Hollnagel's zero-order phenotypes of erroneous action for omissions, jumps, repetitions, and intrusions. Multiple phenotypical acts can occur in sequence, thus allowing for the generation of higher order phenotypes. The task behavior model pattern capable of generating erroneous behavior can be integrated into a formal system model so that system safety properties can be formally verified with a model checker. This allows analysts to prove that a human-automation interactive system (as represented by the model) will or will not satisfy safety properties with both normative and generated erroneous human behavior. We present benchmarks related to the size of the statespace and verification time of models to show how the erroneous human behavior generation process scales. We demonstrate the method with a case study: the operation of a radiation therapy machine. A potential problem resulting from a generated erroneous human action is discovered. A design intervention is presented which prevents this problem from occurring. We discuss how our method could be used to evaluate larger applications and recommend future paths of development.
---
paper_title: Formal Validation of HCI User Tasks

paper_content:

Our work focuses on the use of formal techniques in order to increase the quality of HCI software and of all the processes resulting from the development, verification, design and validation activities. This paper shows how the B formal technique can be used for user tasks modelling and validation. A trace based semantics is used to describe either the HCI or the user tasks. Each task is modelled by a sequence of fired events. Each event is defined in the abstract specification and design of the HCI system.
---
paper_title: AMBOSS: A Task Modeling Approach for Safety-Critical Systems

paper_content:

In a recent project we created AMBOSS, a task modeling environment taking into account the special needs for safety-critical socio-technical systems. An AMBOSS task model allows the specification of relevant information concerning safety aspects. To achieve this we complemented task models with additional information elements and appropriate structures. These refer primarily to aspects of timing, spatial information, and communication. In this paper we give an introductory overview about AMBOSS and its contribution to modeling safety-critical systems. In addition, we present AmbossA, the visual pattern language for detecting particular constellations of interest within a task model.
---
paper_title: Using task analytic models to visualize model checker counterexamples

paper_content:

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

paper_content:

A formal, model-based approach is proposed for the development and evaluation of the sequences of actions specified in procedures. The approach employs methodologies developed within the discipline of discrete-event and hybrid systems control. We demonstrate the proposed approach through an evaluation of a procedure for handling an irregular engine-start on board a modern commercial aircraft. In complex human-machine systems, successful operations depend on an elaborate set of procedures provided to the human operator. These procedures specify a detailed step-by-step process for configuring the machine during normal, abnormal, and emergency situations. The adequacy of these procedures is vitally important for the safe and efficient operation of any complex system. In high-risk endeavors such as aircraft operations, maritime, space flight, nuclear power production, and military operations, it is essential that these procedures be flawless, as the price of error may be unacceptable. When operating procedures are inadequate for the task, not only will the system’s overall efficiency be thwarted, but there may also be tragic human and material
---
paper_title: Integrating model checking and HCI tools to help designers verify user interface properties

paper_content:

In this paper we present a method that aims to integrate the use of formal techniques in the design process of interactive applications, with particular attention to those applications where both usability and safety are main concerns. The method is supported by a set of tools. We will also discuss how the resulting environment can be helpful in reasoning about multi-user interactions using the task model of an interactive application. Examples are provided from a case study in the field of air traffic control.
---
paper_title: Validating Interactive System Design Through the Verification of Formal Task and System Models

paper_content:

This paper addresses the problem of the articulation between task modelling and system modelling in the design of interactive software. We aim at providing solutions allowing the software designers to use efficiently task models during the design process, and to check that the software being built actually corresponds to the requirements elicited during the task analysis phase. The proposed approach is twofold: Firstly, we use the User Action Notation, a semi-formal task modelling formalism, and we present a translation scheme allowing to transform the User Action Notation constructs into Petri nets. Secondly, we use the Interactive Cooperative Objects formalism (based on Petri nets and on the object-oriented approach) to build the model of the system. We finally use the mathematical analysis techniques stemming from the Petri net theory to analyse and validate the cooperation between task models and system model. The approach is presented through a case study, showing the User Action Notation task models, the equivalent Petri net models and the Interactive Cooperative Object system model.
---
paper_title: The UAN: a user-oriented representation for direct manipulation interface designs

paper_content:

Many existing interface representation techniques, especially those associated with UIMS, are constructional and focused on interface implementation, and therefore do not adequately support a user-centered focus. But it is in the behavioral domain of the user that interface designers and evaluators do their work . We are seeking to complement constructional methods by providing a tool-supported technique capable of specifying the behavioral aspects of an interactive system–the tasks and the actions a user performs to accomplish those tasks. In particular, this paper is a practical introduction to use of the User Action Notation (UAN), a task- and user-oriented notation for behavioral representation of asynchronous, direct manipulation interface designs. Interfaces are specified in UAN as a quasihierarchy of asynchronous tasks. At the lower levels, user actions are associated with feedback and system state changes. The notation makes use of visually onomatopoeic symbols and is simple enough to read with little instruction. UAN is being used by growing numbers of interface developers and researchers. In addition to its design role, current research is investigating how UAN can support production and maintenance of code and documentation.
---
paper_title: A Systematic Approach to Model Checking Human–Automation Interaction Using Task Analytic Models

paper_content:

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

paper_content:

We propose a model-based approach to integrate human error analysis with task modelling, introducing the concept of Error Pattern. Error Patterns are prototypical deviations from abstract task models, expressed in a formal way by a model transformation. A collection of typical errors taken from the literature on human errors is described within our framework. The intent is that the human factors specialist will produce the task models taking an error-free perspective, producing small and useful task models. The specialist will then choose from the collection of error patterns, and selectively apply these patterns to parts of the original task model, thus producing a transformed model exhibiting erroneous user behaviour. This transformed task model can be used at various stages of the design process, to investigate the system's reaction to erroneous behaviour or to generate test sequences.
---
paper_title: Specifying and Analyzing Workflows for Automated Identification and Data Capture

paper_content:

Humans use computers to carry out tasks that neither is able to do easily alone: humans provide eyes, hands, and judgment while computers provide computation, networking, and storage. This symbiosis is especially evident in workflows where humans identify objects using bar codes or RFID tags and capture data about them for the computer. This Automated Identification and Data Capture (AIDC) is increasingly important in areas such as inventory systems and health care. Humans involved in AIDC follow simple rules and rely on the computer to catch mistakes; in complex situations this reliance can lead to mismatches between human workflows and system programming. In this paper we explore the design, implementation and formal modeling of AIDC for vital signs measurements in hospitals. To this end we describe the design of a wireless mobile medical mediator device that mediates between identifications, measurements, and updates of Electronic Health Records (EHRs). We implement this as a system Med2 that uses PDAs equipped with Bluetooth, WiFi, and RFID wireless capabilities. Using Communicating Sequential Processes (CSP) we jointly specify workflow and computer system operations and provide a formal analysis of the protections the system provides for user errors.
---
paper_title: ConcurTaskTrees: A Diagrammatic Notation for Specifying Task Models

paper_content:

In this paper we discuss a notation to describe task models, which can specify a wide range of temporal relationships among ta~ks. It is a compact and graphical notation, immediate both to use and understand. Its logical structure and the related automatic tool make it suitable for designing even large sized applications.
---
paper_title: Preventing user errors by systematic analysis of deviations from the system task model

paper_content:

Interactive safety-critical applications have specific requirements that cannot be completely captured by traditional evaluation techniques. In this paper, we discuss how to perform a systematic inspection-based analysis to improve both usability and safety aspects of an application. The analysis considers a system prototype and the related task model and aims to evaluate what could happen when interactions and behaviours occur differently from what the system design assumes. We also provide a description and discussion of an application of this method to a case study in the air traffic control domain.
---
paper_title: Formally verifying human–automation interaction as part of a system model: limitations and tradeoffs

paper_content:

Both the human factors engineering (HFE) and formal methods communities are concerned with improving the design of safety-critical systems. This work discusses a modeling effort that leveraged methods from both fields to perform formal verification of human---automation interaction with a programmable device. This effort utilizes a system architecture composed of independent models of the human mission, human task behavior, human-device interface, device automation, and operational environment. The goals of this architecture were to allow HFE practitioners to perform formal verifications of realistic systems that depend on human---automation interaction in a reasonable amount of time using representative models, intuitive modeling constructs, and decoupled models of system components that could be easily changed to support multiple analyses. This framework was instantiated using a patient controlled analgesia pump in a two phased process where models in each phase were verified using a common set of specifications. The first phase focused on the mission, human-device interface, and device automation; and included a simple, unconstrained human task behavior model. The second phase replaced the unconstrained task model with one representing normative pump programming behavior. Because models produced in the first phase were too large for the model checker to verify, a number of model revisions were undertaken that affected the goals of the effort. While the use of human task behavior models in the second phase helped mitigate model complexity, verification time increased. Additional modeling tools and technological developments are necessary for model checking to become a more usable technique for HFE.
---
paper_title: Evaluating human-automation interaction using task analytic behavior models, strategic knowledge-based erroneous human behavior generation, and model checking

paper_content:

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

paper_content:

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

paper_content:

The development of user interfaces (UI) needs validation and verification of a set of required properties. Different kinds of properties arc relevant to the human computer interaction (HCI) area. Not all of them may be checked using classical software engineering validation and verification tools. Indeed, a large part of properties is related to the user and to usability. Moreover, this kind of properties usually requires an experimental validation. This paper addresses the cooperation between formal and experimental HCI properties validation and verification. It focuses on a proof based technique (event B) and a Model Based System (MBS) based technique (SUIDT). Moreover, this paper tries to bridge the gap between both approaches in order to reduce the heterogeneity they lead to.
---
paper_title: A Method for the Formal Verification of Human-interactive Systems

paper_content:

Predicting failures in complex, human-interactive systems is difficult as they may occur under rare operational conditions and may be influenced by many factors including the system mission, the human operator's behavior, device automation, human-device interfaces, and the operational environment. This paper presents a method that integrates task analytic models of human behavior with formal models and model checking in order to formally verify properties of human-interactive systems. This method is illustrated with a case study: the programming of a patient controlled analgesia pump. Two specifications, one of which produces a counterexample, illustrate the analysis and visualization capabilities of the method.
---
paper_title: Formal socio-technical barrier modelling for safety-critical interactive systems design

paper_content:

Abstract This paper presents a three step approach to improve safety in the field of interactive systems. The approach combines, within a single framework, previous work in the field of barrier analysis and modelling, with model based design of interactive systems. The approach first uses the Safety Modelling Language to specify safety barriers which could achieve risk reduction if implemented. The detailed mechanism by which these barriers behave is designed in the subsequent stage, using a Petri nets-based formal description technique called Interactive Cooperative Objects. One of the main characteristics of interactive systems is the fact that the user is deeply involved in the operation of such systems. This paper addresses this issue of user behaviour by modelling tasks and activities using the same notation as for the system side (both barriers and interactive system). The use of a formal modelling technique for the description of these three components makes it possible to compare, analyse and integrate them. The approach and the integration are presented on a mining case study. Two safety barriers are modelled as well as the relevant parts of the interactive system behaviour. Operators’ tasks are also modelled. The paper then shows how the integration of barriers within the system model can prevent previously identified hazardous sequences of events from occurring, thus increasing the entire system safety.
---
paper_title: A Discrete Control Model of Operator Function: A Methodology for Information Display Design

paper_content:

Recent advances in computer technology and the changing rule of the human in complex systems require changes in design strategies for information displays. The use of discrete control models to represent the human operator's cognitive and decisionmaking activities is described. The analytic procedures required to build a discrete control model show promise as a basis of a design methodology for the definition of an information display system for supervisory control tasks. The discrete control modeling procedures and their application for a simulated system is demonstrated.
---
paper_title: The phenotype of erroneous actions

paper_content:

Abstract The study of human actions with unwanted consequences, in this paper referred to as human erroneous actions, generally suffers from inadequate operational taxonomies. The main reason for this is the lack of a clear distinction between manifestations and causes. The failure to make this distinction is due to the reliance on subjective evidence which unavoidably mixes manifestations and causes. The paper proposes a clear distinction between the phenotypes (manifestations) and the genotypes (causes) of erroneous actions. A logical set of phenotypes is developed and compared with the established "human error" taxonomies as well as with the operational categories which have been developed in the field of human reliability analysis. The principles for applying the set of phenotypes as practical classification criteria are developed and described. A further illustration is given by the report of an action monitoring system (RESQ) which has been implemented as part of a larger set of operator support systems and which shows the viability of the concepts. The paper concludes by discussing the principal issues of error detection, in particular the trade-off between precision and meaningfulness.
---
paper_title: Programmable user models for predictive evaluation of interface designs

paper_content:

A Programmable User Model (PUM) is a psychologically constrained architecture which an interface designer is invited to program to simulate a user performing a range of tasks with a proposed interface. It provides a novel way of conveying psychological considerations to the designer, by involving the designer in the process of making predictions of usability. Development of the idea leads to a complementary perspective, of the PUM as an interpreter for an “instruction language”. The methodology used in this research involves the use of concrete HCI scenarios to assess different approaches to cognitive modelling. The research findings include analyses of the cognitive processes involved in the use of interactive computer systems, and a number of issues to be resolved in future cognitive models.
---
paper_title: Model-checking user behaviour using interacting components

paper_content:

This article describes a framework to formally model and analyse human behaviour. This is shown by a simple case study of a chocolate vending machine, which represents many aspects of human behaviour. The case study is modelled and analysed using the Maude rewrite system. This work extends a previous work by Basuki which attempts to model interactions between human and machine and analyse the possibility of errors occurring in the interactions. By redesigning the interface, it can be shown that certain kinds of error can be avoided for some users. This article overcomes the limitation of Basuki’s approach by incorporating many aspects of user behaviour into a single user model, and introduces a more natural approach to model human–computer interaction.
---
paper_title: Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors

paper_content:

Interactive systems combine a human operator with a computer. Either may be a source of error. The verification processes used must ensure both the correctness of the computer component, and also minimize the risk of human error. Human-centred design aims to do this by designing systems in a way that make allowance for human frailty. One approach to such design is to adhere to design rules. Design rules, however, are often ad hoc. We examine how a formal cognitive model, encapsulating results from the cognitive sciences, can be used to justify such design rules in a way that integrates their use with existing formal hardware verification techniques. We consider here the verification of a design rule intended to prevent a commonly occurring class of human error know as the post-completion error.
---
paper_title: Modelling Distributed Cognition Systems in PVS

paper_content:

We report on our efforts to formalise DiCoT, an informal structured approach for analysing complex work systems, such as hospital and day care units, as distributed cognition systems. We focus on DiCoT's information flow model, which describes how information is transformed and propagated in the system. Our contribution is a set of generic models for the specification and verification system PVS. The developed models can be directly mapped to the informal descriptions adopted by human-computer interactions experts. The models can be verified against properties of interest in the PVS theorem prover. Also, the same models can be simulated, thus facilitating analysts to engage with stakeholders when checking the correctness of the model. We trial our ideas on a case study based on a real-world medical system.
---
paper_title: Models of interactive systems : a case study on Programmable User Modelling

paper_content:

Models of interactive systems can be used to answer focused questions about those systems. Making the appropriate choice of modelling technique depends on what questions are being asked. We present two styles of interactive system model and associated verification method. We show how they contrast in terms of tractability, inspectability of assumptions, level of abstraction and reusability of model fragments. These trade-offs are discussed. We discuss how they can be used as part of an integrated formal approach to the analysis of interactive systems where the different formal techniques focus on specific problems raised by empirical investigations. Explanations resulting from the formal analyses can be validated with respect to the empirical data.The first modelling style, which we term 'operational', is derived directly from principles of rationality that constrain which user behaviours are modelled. Modelling involves laying out user knowledge of the system and task, and their goals, then applying the principles to reason about the space of rational behaviours. This style supports reasoning about user knowledge and the consequences of particular knowledge in terms of likely behaviours. It is well suited to reasoning about interactions where user knowledge is a key to successful interaction. Such models can readily be implemented as computer programs; one such implementation is presented here.Models of the second style, 'abstract', are derived from the operational models and thus retain important aspects of rationality. As a result of the simplification, mathematical proof about selected properties of the interactive system, such as safety properties, can be tractably applied to these models. This style is well suited to cases where the user adopts particular strategies that can be represented succinctly within the model.We demonstrate the application of the two styles for understanding a reported phenomenon, using a case study on electronic diaries.
---
paper_title: Formal Modelling of Salience and Cognitive Load ⋆

paper_content:

Well-designed interfaces use procedural and sensory cues to increase the salience of appropriate actions and intentions. However, empirical studies suggest that cognitive load can influence the strength of procedural and sensory cues. We formalise the relationship between salience and cognitive load revealed by empirical data. We add these rules to our abstract cognitive architecture developed for the verification of usability properties. The interface of a fire engine dispatch task used in the empirical studies is then formally verified to assess the salience and load rules. Finally, we discuss how the formal modelling and verification suggests further refinements of the rules derived from the informal analysis of empirical data.
---
paper_title: Demonstrating the Cognitive Plausibility of Interactive System Specifications

paper_content:

Much of the behaviour of an interactive system is determined by its user population. This paper describes how assumptions about the user can be brought into system models in order to reason about their behaviour. We describe a system model containing reasonable assumptions about the user as being ‘cognitively plausible’. Before asserting the plausibility of a model however we must first be able to make the assumptions made in that model inspectable.
---
paper_title: Formal Modelling of Cognitive Interpretation

paper_content:

We formally specify the interpretation stage in a dual state space human-computer interaction cycle. This is done by extending / reorganising our previous cognitive architecture. In particular, we focus on shape related aspects of the interpretation process associated with device input prompts. A cash-point example illustrates our approach. Using the SAL model checking environment, we show how the extended cognitive architecture facilitates detection of prompt-shape induced human error.
---
paper_title: Formal analysis of human-computer interaction using model-checking

paper_content:

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.
---
paper_title: Users as rational interacting agents: formalising assumptions about cognition and interaction

paper_content:

One way of assessing the usability of a computer system is to make reasonable assumptions about users’ cognition and to analyse how they can be expected to work with the system, using their knowledge and information from the display to achieve their goals. This is the approach taken in Programmable User Modelling Analysis, a technique for predictive usability evaluation of interactive systems. The technique is based on the premise that an analyst can gain insights into the usability of a computer system by specifying the knowledge that a user needs to be able to use it and drawing inferences on how that knowledge will guide the user’s behaviour. This may be done by observing how a cognitive architecture, “programmed” with that knowledge, behaves. An alternative approach is to develop a formal description of the essential features of the cognitive architecture and to use that description to reason about likely user behaviour. In this paper, we present the approach and an outline formal description of the cognitive architecture. This initial description is derived from an existing implementation. We illustrate how the description can be used in reasoning by applying it to the task of setting up call diverting on a mobile phone. Successful performance of this task involves a combination of planned and responsive behaviour. The process of doing this analysis highlights what assumptions have been made by the designers about the user’s knowledge. We discuss limitations of the current formalisation and identify directions for future work.
---
paper_title: Verification-guided modelling of salience and cognitive load

paper_content:

Well-designed interfaces use procedural and sensory cues to increase the cognitive salience of appropriate actions. However, empirical studies suggest that cognitive load can influence the strength of those cues. We formalise the relationship between salience and cognitive load revealed by empirical data. We add these rules to our abstract cognitive architecture, based on higher-order logic and developed for the formal verification of usability properties. The interface of a fire engine dispatch task from the empirical studies is then formally modelled and verified. The outcomes of this verification and their comparison with the empirical data provide a way of assessing our salience and load rules. They also guide further iterative refinements of these rules. Furthermore, the juxtaposition of the outcomes of formal analysis and empirical studies suggests new experimental hypotheses, thus providing input to researchers in cognitive science.
---
paper_title: From a Formal User Model to Design Rules

paper_content:

Design rules sometimes seem to contradict. We examine how a formal description of user behaviour can help explain the context when such rules are, or are not, applicable. We describe how they can be justified from a formally specified generic user model. This model was developed by formalising cognitively plausible behaviour, based on results from cognitive psychology. We examine how various classes of erroneous actions emerge from the underlying model. Our lightweight semiformal reasoning from the user model makes predictions that could be used as the basis for further usability studies. Although the user model is very simple, a range of error patterns and design principles emerge.
---
paper_title: An approach to formal verification of human–computer interaction

paper_content:

The correct functioning of interactive computer systems depends on both the faultless operation of the device and correct human actions. In this paper, we focus on system malfunctions due to human actions. We present abstract principles that generate cognitively plausible human behaviour. These principles are then formalised in a higher-order logic as a generic, and so retargetable, cognitive architecture, based on results from cognitive psychology. We instantiate the generic cognitive architecture to obtain specific user models. These are then used in a series of case studies on the formal verification of simple interactive systems. By doing this, we demonstrate that our verification methodology can detect a variety of realistic, potentially erroneous actions, which emerge from the combination of a poorly designed device and cognitively plausible human behaviour.
---
paper_title: Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking

paper_content:

Breakdowns in complex systems often occur as a result of system elements interacting in unanticipated ways. In systems with human operators, human-automation interaction associated with both normative and erroneous human behavior can contribute to such failures. Model-driven design and analysis techniques provide engineers with formal methods tools and techniques capable of evaluating how human behavior can contribute to system failures. This paper presents a novel method for automatically generating task analytic models encompassing both normative and erroneous human behavior from normative task models. The generated erroneous behavior is capable of replicating Hollnagel's zero-order phenotypes of erroneous action for omissions, jumps, repetitions, and intrusions. Multiple phenotypical acts can occur in sequence, thus allowing for the generation of higher order phenotypes. The task behavior model pattern capable of generating erroneous behavior can be integrated into a formal system model so that system safety properties can be formally verified with a model checker. This allows analysts to prove that a human-automation interactive system (as represented by the model) will or will not satisfy safety properties with both normative and generated erroneous human behavior. We present benchmarks related to the size of the statespace and verification time of models to show how the erroneous human behavior generation process scales. We demonstrate the method with a case study: the operation of a radiation therapy machine. A potential problem resulting from a generated erroneous human action is discovered. A design intervention is presented which prevents this problem from occurring. We discuss how our method could be used to evaluate larger applications and recommend future paths of development.
---
paper_title: Modelling Distributed Cognition Systems in PVS

paper_content:

We report on our efforts to formalise DiCoT, an informal structured approach for analysing complex work systems, such as hospital and day care units, as distributed cognition systems. We focus on DiCoT's information flow model, which describes how information is transformed and propagated in the system. Our contribution is a set of generic models for the specification and verification system PVS. The developed models can be directly mapped to the informal descriptions adopted by human-computer interactions experts. The models can be verified against properties of interest in the PVS theorem prover. Also, the same models can be simulated, thus facilitating analysts to engage with stakeholders when checking the correctness of the model. We trial our ideas on a case study based on a real-world medical system.
---
paper_title: Capturing the distinction between task and device errors in a formal model of user behaviour

paper_content:

In any complex interactive human-computer system, people are likely to make errors during its operation. In this paper, we describe a validation study of an existing generic model of user behaviour. The study is based on the data and conclusions from an independent prior experiment. We show that the current model does successfully capture the key concepts investigated in the experiment, particularly relating to results to do with the distinction between task and device-specific errors. However, we also highlight some apparent weaknesses in the current model with respect to initialisation errors, based on comparison with previously unpublished (and more detailed) data from the experiment. The differences between data and observed model behaviour suggest the need for new empirical research to determine what additional factors are at work. We also discuss the potential use of formal models of user behaviour in both informing, and generating further hypotheses about the causes of human error.
---
paper_title: Validating Human-device Interfaces with Model Checking and Temporal Logic Properties Automatically Generated from Task Analytic Models

paper_content:

When evaluating designs of human-device interfaces for safety critical systems, it is very important that they be valid: support the goal-directed tasks they were designed to facilitate. Model checking is a type of formal analysis that is used to mathematically prove whether or not a model of a system does or does not satisfy a set of specification properties, usually written in a temporal logic. In the analysis of human-automation interaction, model checkers have been used to formally verify that human-device interface models are valid with respect to goal-directed tasks encoded in temporal logic properties. All of the previous work in this area has required that analysts manually specify these properties. Given the semantics of temporal logic and the complexity of task analytic behavior models, this can be very difficult. This paper describes a method that allows temporal logic properties to be automatically generated from task analytic models created early in the system design process. This allows analysts to use model checkers to validate that modeled human-device interfaces will allow human operators to successfully perform the necessary tasks with the system. The use of the method is illustrated with a patient controlled analgesia pump programming example. The method is discussed and avenues for future work are described.
---
paper_title: A Systematic Approach to Model Checking Human–Automation Interaction Using Task Analytic Models

paper_content:

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

paper_content:

Human-computer interaction (HCI) systems control an ongoing interaction between end-users and computer-based systems. For software-intensive systems, a graphic user interface (GUI) is often employed for enhanced usability. Traditional approaches to validation of GUI aspects in HCI systems involve prototyping and live-subject testing. These approaches are limited in their ability to cover the set of possible human-computer interactions that a system may allow, since patterns of interaction may be long running and have large numbers of alternatives. In this paper, we propose a static analysis that is capable of reasoning about user-interaction properties of GUI portions of HCI applications written in Java using modern GUI frameworks, such as Swing/spl trade/. Our approach consists of partitioning an HCI application into three parts: the Swing library, the GUI implementation, i.e., code that interacts directly with Swing, and the underlying application. We develop models of each of these parts that preserve behavior relevant to interaction ordering. We describe how these models are generated and how we have customized a model checking framework to efficiently analyze their combination.
---
paper_title: Formally verifying human–automation interaction as part of a system model: limitations and tradeoffs

paper_content:

Both the human factors engineering (HFE) and formal methods communities are concerned with improving the design of safety-critical systems. This work discusses a modeling effort that leveraged methods from both fields to perform formal verification of human---automation interaction with a programmable device. This effort utilizes a system architecture composed of independent models of the human mission, human task behavior, human-device interface, device automation, and operational environment. The goals of this architecture were to allow HFE practitioners to perform formal verifications of realistic systems that depend on human---automation interaction in a reasonable amount of time using representative models, intuitive modeling constructs, and decoupled models of system components that could be easily changed to support multiple analyses. This framework was instantiated using a patient controlled analgesia pump in a two phased process where models in each phase were verified using a common set of specifications. The first phase focused on the mission, human-device interface, and device automation; and included a simple, unconstrained human task behavior model. The second phase replaced the unconstrained task model with one representing normative pump programming behavior. Because models produced in the first phase were too large for the model checker to verify, a number of model revisions were undertaken that affected the goals of the effort. While the use of human task behavior models in the second phase helped mitigate model complexity, verification time increased. Additional modeling tools and technological developments are necessary for model checking to become a more usable technique for HFE.
---
paper_title: Evaluating human-automation interaction using task analytic behavior models, strategic knowledge-based erroneous human behavior generation, and model checking

paper_content:

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

paper_content:

Abstract This paper presents a design framework for safety critical interactive systems, based on a formal description technique called the ICO (Interactive Cooperative Object) formalism. ICO allows for describing, in a formal way, all the components of highly interactive (also called post-WIMP) applications. The framework is supported by a case tool called PetShop allowing for editing, verifying and executing the formal models. The first section describes why such user interfaces are challenging for most description techniques, as well as the state of the art in this field. Section 3 presents a development process dedicated to the framework. Then, we use a case study in order to recall the basic concepts of the ICO formalism and the recent extensions added in order to take into account post-WIMP interfaces' specificities. Section 5 presents the case tool PetShop and how the case study presented in the previous section has been dealt with. Lastly, we show how PetShop can be used for interactive prototyping.
---
paper_title: Designing Safe, Reliable Systems using Scade

paper_content:

As safety critical systems increase in size and complexity, the need for efficient tools to verify their reliability grows. In this paper we present a tool that helps engineers design safe and reliable systems. Systems are reliable if they keep operating safely when components fail. Our tool is at the core of the Scade Design Verifier integrated within Scade, a product developed by Esterel Technologies. Scade includes a graphical interface to build formal models in the synchronous data-flow language Lustre. Our tool automatically extends Lustre models by injecting faults, using libraries of typical failures. It allows to perform Failure Mode and Effect Analysis, which consists of verifying whether systems remain safe when selected components fail. The tool can also compute minimal combinations of failures breaking systems' safety, which is similar to Fault Tree Analysis. The paper includes successful verifications of examples from the aeronautics industry.
---
paper_title: Formal and experimental validation approaches in HCI systems design based on a shared event B model

paper_content:

The development of user interfaces (UI) needs validation and verification of a set of required properties. Different kinds of properties arc relevant to the human computer interaction (HCI) area. Not all of them may be checked using classical software engineering validation and verification tools. Indeed, a large part of properties is related to the user and to usability. Moreover, this kind of properties usually requires an experimental validation. This paper addresses the cooperation between formal and experimental HCI properties validation and verification. It focuses on a proof based technique (event B) and a Model Based System (MBS) based technique (SUIDT). Moreover, this paper tries to bridge the gap between both approaches in order to reduce the heterogeneity they lead to.
---
paper_title: Automatic detection of interaction vulnerabilities in an executable specification

paper_content:

This paper presents an approach to providing designers with the means to detect Human-Computer Interaction (HCI) vulnerabilities without requiring extensive HCI expertise. The goal of the approach is to provide timely, useful analysis results early in the design process, when modifications are less expensive. The twin challenges of providing timely and useful analysis results led to the development and evaluation of computational analyses, integrated into a software prototyping toolset. The toolset, referred to as the Automation Design and Evaluation Prototyping Toolset (ADEPT) was constructed to enable the rapid development of an executable specification for automation behavior and user interaction. The term executable specification refers to the concept of a testable prototype whose purpose is to support development of a more accurate and complete requirements specification.
---
paper_title: Incident and Accident Investigation Techniques to Inform Model-Based Design of Safety-Critical Interactive Systems

paper_content:

The quality of the design of an interactive safety-critical system can be enhanced by embedding data and knowledge from past experiences. Traditionally, this involves applying scenarios, usability analysis, or the use of metrics for risk analysis. In this paper, we present an approach that uses the information from incident investigations to inform the development of safety-cases that can, in turn, be used to inform a formal system model, represented using Petri nets and the ICO formalism. The foundations of the approach are first detailed and then exemplified using a fatal mining accident case study.
---
paper_title: Lightweight Formal Methods

paper_content:

Formal methods have offered great benefits, but often at a heavy price. For everyday software development, in which the pressures of the market don't allow full-scale formal methods to be applied, a more lightweight approach is called for. I'll outline an approach that is designed to provide immediate benefit at relatively low cost. Its elements are a small and succinct modelling language, and a fully automatic analysis scheme that can perform simulations and find errors. I'll describe some recent case studies using this approach, involving naming schemes, architectural styles, and protocols for networks with changing topologies. I'll make some controversial claims about this approach and its relationship to UML and traditional formal specification approaches, and I'll barbeque some sacred cows, such as the belief that executability compromises abstraction.
---
paper_title: Interaction engineering using the IVY tool

paper_content:

This paper is concerned with support for the process of usability engineering. The aim is to use formal techniques to provide a systematic approach that is more traceable, and because it is systematic, repeatable. As a result of this systematic process some of the more subjective aspects of the analysis can be removed. The technique explores exhaustively those features of a specific design that fail to satisfy a set of properties. It also analyzes those aspects of the design where it is possible to quantify the cost of use. The method is illustrated using the example of a medical device. While many aspects of the approach and its tool support have already been discussed elsewhere, this paper builds on and contrasts an analysis of the same device provided by a third party and in so doing enhances the IVY tool.
---
paper_title: Formal Modeling and Analysis for Interactive Hybrid Systems

paper_content:

An effective strategy for discovering certain kinds of automation surprise and other problems in interactive systems is to build models of the participating (automated and human) agents and then explore all reachable states of the composed system looking for divergences between mental states and those of the automation. Various kinds of model checking provide ways to automate this approach when the agents can be modeled as discrete automata. But when some of the agents are continuous dynamical systems (e.g., airplanes), the composed model is a hybrid (i.e., mixed continuous and discrete) system and these are notoriously hard to analyze. We describe an approach for very abstract modeling of hybrid systems using rela- tional approximations and their automated analysis using infinite bounded model checking supported by an SMT solver. When counterexamples are found, we de- scribe how additional constraints can be supplied to direct counterexamples toward plausible scenarios that can be confirmed in high-fidelity simulation. The approach is illustrated though application to a known (and now corrected) human-automation interaction problem in Airbus aircraft.
---
paper_title: Adaptive Automation of a Dynamic Control Task Based on Secondary Task Workload Measurement

paper_content:

Adaptive automation (AA) has been proposed as a method for regulating human workload and abating out-of-the-loop performance problems in complex systems control. The majority of AA or adaptive manual control studies, to this point, have facilitated control allocations using either preprogrammed schemes based on desired system performance, comparisons of human performance with established goals, or psychophysical variable monitoring to represent workload levels and determine appropriate control allocations for moderating workload. This study further explored the psychophysical assessment approach by using a secondary task measure of workload to facilitate control allocations in a complex primary task. An experiment was conducted in which participants performed a secondary gauge-monitoring task along with a simulated radar monitoring and target elimination task. Differences in single-secondary task performance and performance observed while also functioning in the primary task were used to direct operator-m...
---
paper_title: Trust, control strategies and allocation of function in human-machine systems.

paper_content:

As automated controllers supplant human intervention in controlling complex systems, the operators' role often changes from that of an active controller to that of a supervisory controller. Acting as supervisors, operators can choose between automatic and manual control. Improperly allocating function between automatic and manual control can have negative consequences for the performance of a system. Previous research suggests that the decision to perform the job manually or automatically depends, in part, upon the trust the operators invest in the automatic controllers. This paper reports an experiment to characterize the changes in operators' trust during an interaction with a semi-automatic pasteurization plant, and investigates the relationship between changes in operators' control strategies and trust. A regression model identifies the causes of changes in trust, and a 'trust transfer function' is developed using time series analysis to describe the dynamics of trust. Based on a detailed analysis of operators' strategies in response to system faults we suggest a model for the choice between manual and automatic control, based on trust in automatic controllers and self-confidence in the ability to control the system manually.
---
paper_title: Human-Automated Judge Learning: A Methodology for Examining Human Interaction With Information Analysis Automation

paper_content:

Human-automated judge learning (HAJL) is a methodology providing a three-phase process, quantitative measures, and analytical methods to support design of information analysis automation. HAJL's measures capture the human and automation's judgment processes, relevant features of the environment, and the relationships between each. Specific measures include achievement of the human and the automation, conflict between them, compromise and adaptation by the human toward the automation, and the human's ability to predict the automation. HAJL's utility is demonstrated herein using a simplified air traffic conflict prediction task. HAJL was able to capture patterns of behavior within and across the three phases with measures of individual judgments and human-automation interaction. Its measures were also used for statistical tests of aggregate effects across human judges. Two between-subject manipulations were crossed to investigate HAJL's sensitivity to interventions in the human's training (sensor noise during training) and in display design (information from the automation about its judgment strategy). HAJL identified that the design intervention impacted conflict and compromise with the automation, participants learned from the automation over time, and those with higher individual judgment achievement were also better able to predict the automation.
---
paper_title: ACT-R: a theory of higher level cognition and its relation to visual attention

paper_content:

The ACT-R system is a general system for modeling a wide range of higher level cognitive processes. Recently, it has been embellished with a theory of how its higher level processes interact with a visual interface. This includes a theory of how visual attention can move across the screen, encoding information into a form that can be processed by ACT-R. This system is applied to modeling several classic phenomena in the literature that depend on the speed and selectivity with which visual attention can move across a visual display. ACT-R is capable of interacting with the same computer screens that subjects do and, as such, is well suited to provide a model for tasks involving human-computer interaction. In this article, we discuss a demonstration of ACT-R's application to menu selection and show that the ACT-R theory makes unique predictions, without estimating any parameters, about the time to search a menu. These predictions are confirmed.
---
paper_title: Using GOMS for user interface design and evaluation: which technique?

paper_content:

Since the seminal book, The Psychology of Human-Computer Interaction , the GOMS model has been one of the few widely known theoretical concepts in human-computer interaction. This concept has spawned much research to verify and extend the original work and has been used in real-world design and evaluation situations. This article synthesizes the previous work on GOMS to provide an integrated view of GOMS models and how they can be used in design. We briefly describe the major variants of GOMS that have matured sufficiently to be used in actual design. We then provide guidance to practitioners about which GOMS variant to use for different design situations. Finally, we present examples of the application of GOMS to practical design problems and then summarize the lessons learned.
---
paper_title: Toward a multi-method approach to formalizing human-automation interaction and human-human communications

paper_content:

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

paper_content:

We propose algorithms which combine simulation with symbolic methods for the verification of invariants. The motivation is two-fold. First, there are designs which are too complex to be formally verified using symbolic methods; however the use of symbolic techniques in conjunction with traditional simulation results in better “coverage” relative to the computational resources used. Additionally, even on designs which can be symbolically verified, the use of a hybrid methodology often detects the presence of bugs faster than either formal verification or simulation.
---
paper_title: Spatial Awareness in Synthetic Vision Systems: Using Spatial and Temporal Judgments to Evaluate Texture and Field of View

paper_content:

OBJECTIVE ::: This work introduced judgment-based measures of spatial awareness and used them to evaluate terrain textures and fields of view (FOVs) in synthetic vision system (SVS) displays. ::: ::: ::: BACKGROUND ::: SVSs are cockpit technologies that depict computer-generated views of terrain surrounding an aircraft. In the assessment of textures and FOVs for SVSs, no studies have directly measured the three levels of spatial awareness with respect to terrain: identification of terrain, its relative spatial location, and its relative temporal location. ::: ::: ::: METHODS ::: Eighteen pilots made four judgments (relative azimuth angle, distance, height, and abeam time) regarding the location of terrain points displayed in 112 noninteractive 5-s simulations of an SVS head-down display. There were two between-subject variables (texture order and FOV order) and five within-subject variables (texture, FOV, and the terrain point's relative azimuth angle, distance, and height). ::: ::: ::: RESULTS ::: Texture produced significant main and interaction effects for the magnitude of error in the relative angle, distance, height, and abeam time judgments. FOV interaction effects were significant for the directional magnitude of error in the relative distance, height, and abeam time judgments. ::: ::: ::: CONCLUSION ::: Spatial awareness was best facilitated by the elevation fishnet (EF), photo fishnet (PF), and photo elevation fishnet (PEF) textures. ::: ::: ::: APPLICATION ::: This study supports the recommendation that the EF, PF, and PEF textures be further evaluated in future SVS experiments. Additionally, the judgment-based spatial awareness measures used in this experiment could be used to evaluate other display parameters and depth cues in SVSs.
---
paper_title: Simulation vs. formal: absorb what is useful; reject what is useless

paper_content:

This short paper is the result of the invited talk I gave at the 2007 Haifa Verification Conference. Its purpose is to briefly summarize the main points of my talk and to provide background references. The original talk abstract was, "Dynamic verification (simulation, emulation) and formal verification often live in separate worlds, with minimal interaction between the two camps, yet both have unique strengths that could complement the other. In this talk, I'll briefly enumerate what I believe are the best aspects of each verification style, and then explore some possibilities for drawing on the strengths of both camps."
---
paper_title: Combining Human Error Verification and Timing Analysis

paper_content:

Designs can often be unacceptable on performance grounds. In this work, we integrate a GOMS-like ability to predict execution times into the generic cognitive architecture developed for the formal verification of human error related correctness properties. As a result, formal verification and GOMS-like timing analysis are combined within a unified framework. This allows one to judge whether a formally correct design is also acceptable on performance grounds, and vice versa. We illustrate our approach with an example based on a KLM style timing analysis.
---

Title: Using Formal Verification to Evaluate Human-Automation Interaction: A Review

Section 1: Introduction
Description 1: Introduce the topic of formal verification and its relevance to human-automation interaction (HAI), providing background and setting the stage for the review.

Section 2: Formal Verification
Description 2: Explain the principles of formal verification, including techniques such as automated theorem proving and model checking, and discuss their application in ensuring system correctness.

Section 3: Formal Verification of Human-Automation Interaction
Description 3: Review how formal verification has been applied to HAI, highlighting various studies and approaches used to address issues like usability and mode confusion in human-automation systems.

Section 4: Formal Verification of Human-Automation Interface Properties
Description 4: Discuss the use of formal verification specifically for evaluating properties of human-automation interfaces, including usability and mode confusion analyses.

Section 5: Formal Verification Using Human Models
Description 5: Explore approaches that incorporate models of human cognitive and task behavior in formal verification to predict and analyze HAI failures and system-level problems.

Section 6: Discussion and Future Development
Description 6: Summarize the findings of the review, discuss the limitations and tradeoffs of different formal verification techniques, and suggest directions for future research and development.