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

摘要

Automatic behaviour can be defined as a fast processinghuman activity that does not require attention to occur.According to Norman and Shallice's model of attention andautomaticity the majority of responses are under fairly automaticcontrol triggered by environmental cues.In this paper we define a process algebraic framework toformalise Norman and Shallice's model and illustrate it throughtwo case studies: Driving and using an Automatic TellerMachine (ATM).Finally we show how to use model-checking to analyse modelinstantiations and present the outcome of the analysis for theATM case study.