Improving the scalability of formal human–automation interaction verification analyses that use task-analytic models

The enhanced operator function model with communications (EOFMCs) is a task-analytic modeling formalism used for including human behavior in formal models of larger systems. This allows the contribution of human behavior to the safety of the system to be evaluated with model checking. The previous m...

Full description

Saved in:
Bibliographic Details
Published in:Innovations in systems and software engineering 2017-03, Vol.13 (1), p.1-17
Main Authors: Bolton, Matthew L., Zheng, Xi, Molinaro, Kylie, Houser, Adam, Li, Meng
Format: Article
Language:English
Subjects:
Artificial Intelligence
Computer Applications
Computer Science
Human behavior
Original Paper
Software Engineering
Translating
Verification
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:The enhanced operator function model with communications (EOFMCs) is a task-analytic modeling formalism used for including human behavior in formal models of larger systems. This allows the contribution of human behavior to the safety of the system to be evaluated with model checking. The previous method for translating the EOFMCs into model checker input language was conceptually straightforward, but extremely statespace inefficient. This limited the applications that could be formally verified using EOFMC. In this paper, we present an alternative approach for formally representing EOFMCs that substantially decreases the model’s statespace size and verification time. This paper motivates this effort, describes how the improvement was achieved, presents benchmarks demonstrating the improvements in statespace size and verification time, discusses the implications of these results, and outlines directions for future improvement.
ISSN:1614-5046
1614-5054
DOI:10.1007/s11334-016-0272-z