Logo image
Back
Formally verifying human-automation interaction as part of a system model: limitations and tradeoffs
Journal article   Open access   Peer reviewed

Formally verifying human-automation interaction as part of a system model: limitations and tradeoffs

Matthew L. Bolton and Ellen J. Bass
Innovations in systems and software engineering, v 6(3), pp 219-231
01 Sep 2010
DOI: https://doi.org/10.1007/s11334-010-0129-9
PMID: 21572930
url
https://doi.org/10.1007/s11334-010-0129-9View
Published, Version of Record (VoR)CC BY-NC V4.0,  Open

Abstract

Computer Science Computer Science, Software Engineering Science & Technology Technology
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 phasewere 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.

Metrics

1 Record Views
36 citations in Web of Science
49 citations in Scopus

Details

InCites Highlights

Data related to this publication, from InCites Benchmarking & Analytics tool:

Web of Science research areas
Computer Science, Software Engineering
Logo image