A formal method for assessing the impact of task-based erroneous human behavior on system safety

•Erroneous human behavior is a major contributor to system failure.•We introduce a method for generating erroneous behaviors in model checking analyses.•We use case studies to show that our method can find both known and unknown failures.•Case studies include medical devices and an Apache helicopter...

Full description

Saved in:
Bibliographic Details
Published in:Reliability engineering & system safety 2019-08, Vol.188, p.168-180
Main Authors: Bolton, Matthew L., Molinaro, Kylie A., Houser, Adam M.
Format: Article
Language:English
Subjects:
Automation
Erroneous human behavior
Formal method
Formal methods
Helicopters
Human behavior
Human error
Pain
Radiation
Radiation therapy
Reliability engineering
System failures
System safety
Task analysis
Taxonomy
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:•Erroneous human behavior is a major contributor to system failure.•We introduce a method for generating erroneous behaviors in model checking analyses.•We use case studies to show that our method can find both known and unknown failures.•Case studies include medical devices and an Apache helicopter firing procedure. Erroneous human behavior is often cited as a major factor to system failure. However, the complexity of the human-automation interaction can make it difficult for engineers to anticipate how erroneous human behavior can contribute to failures. In this work, we introduce a novel method for generating human errors based on the task-based taxonomy of erroneous human behavior. This allows erroneous acts to manifest as divergences from task models. We implement our method using the Enhanced Operator Function Model. We further show how the method can be used with formal system modeling and formal verification with model checking to prove whether or not potentially unanticipated erroneous behavior could contribute to system failures. We evaluate how our method scales and use it to evaluate three case studies: a radiation therapy machine, a pain medication pump, and an Apache helicopter. We discuss these results and explore options for future work.
ISSN:0951-8320
1879-0836
DOI:10.1016/j.ress.2019.03.010