A Formal Method for Assessing Mental Workload.

Mental workload extremes are associated with poor human performance and safety problems across safety critical domains. Mental workload is a complex, difficult-to-predict phenomenon, where issues may only arise due to concurrency between resource-conflicting tasks. This research addresses this deficiency by presenting a novel method for using model checking (for performing formal proofs about concurrent systems) to predict mental workload. Our method combines multiple resource theory and formal methods based on hierarchical task analysis to identify mental workload extremes in a complex system. This paper presents this method and shows preliminary validation using a texting and driving task. Implications of our results and future research are discussed.