Closure and Attention Activation in Human Automatic Behaviour: A Framework for the Formal Analysis of Interactive Systems

Abstract

Automatic behaviour can be defined as a fast processing
human activity that does not require attention to occur.
According to Norman and Shallice's model of attention and
automaticity the majority of responses are under fairly automatic
control triggered by environmental cues.
In this paper we define a process algebraic framework to
formalise Norman and Shallice's model and illustrate it through
two case studies: Driving and using an Automatic Teller
Machine (ATM).
Finally we show how to use model-checking to analyse model
instantiations and present the outcome of the analysis for the
ATM case study.