# Presentation: 328303

## Formal Modeling of Erroneous Human Behavior and its Implications for Model Checking 

- Matthew L. Bolton and Ellen J. Bass
- University of Virginia
- Department of Systems and
- Information Engineering

## System Failure

- Modern system exhibit interaction between:
- Technological infrastructure (including subsystems, automation, human-system interfaces)
- People (such as operators, maintenance crews)
- Operational environment
- Well engineered infrastructure at an individual level (sometimes)
- Emergent system failure: the interaction between components can result in unforeseen problems

- Latent / Active Failures

## System Failure and Human Error 

- Human Error contributes to:
- Between 44,000 and 98,000 deaths nationwide in medical practice
- 75.5 % of all general aviation accidents
- High profile accidents:
- Challenger
- Three mile island
- Therac-25
- Exxon Valdese

**D’oh!**

## Predicting System Failure: Model Checking

## Formal Modeling of Human-system Interfaces

- Human-system Interface

- Formal Model of Interface

## Normative Models of Human Behavior (OFM)

## Hollnagel’s Phenotypes of Human Error

- All observable human errors are composed of the following erroneous acts:
- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action
- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (an intrusion)

## Research Goal

- To develop a methodology that integrates:
- Formal system models,
- Formal models of the human-system interfaces,
- Human behavior models,
- Models of erroneous human behavior, and
- Model checking verification
- 	to identify potential latent errors that may be preconditions to system failure

## Failure Prediction Framework

## Failure Prediction Framework

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

- Becomes

- Becomes

- Becomes

- Becomes

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

**b** Becomes

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

## Human Error Prediction and Modeling

- Prematurely starting an action
- Delayed start of an action
- Prematurely finishing an action
- Omitting an action
- Skipping an action

- Re-performing a previously completed action
- Repeating the current action
- Performing an unplanned action (intrusion)

- Hollnagel’s Phenotypes

## Example 

- Interface

- Formal Model of Interface

- Normative Human Behavior Model

- Erroneous Human Behavior Model

## Implications: Model Reduction

- Possible model reduction by using constraints based on plausible human behavior and detection of latent errors to remove unnecessary states.

## Implications: Explanation

- Counter Example

- The erroneous human behavior model can illustrate how human behavior contributed to system failures seen in model checker counter examples
- May elucidate design solutions: forcing functions, training, interface designs, etc.

## Questions