Formal Methods and Human Cognition

Formal methods have been largely applied to the verification of functional correctness as well as safety and security properties of computer systems. However, in most cases the verification results make sense only under the assumption that the user interacts with the system exactly in the way specified by the system designer. Moreover, only human errors that are explicitly addressed by the specification or explicitly incorporated in the system model may be captured by the formal verification process. Nowadays, as a consequence of ubiquitous computing and widespread technology, there is a large variation in the typology and motivations of humans interacting with computer systems. This makes it impossible to define a predicted user's behaviour: human errors are actually the very result of an unexpected user behaviour that emerges through the interaction. In this seminar we present a framework to incorporate cognitive processes underlying human behaviour within the formal model of an interactive system. We focus on everyday human activities, in which the majority of responses are under fairly automatic control. This is the context in which cognitive errors are most likely to occur. We illustrate how to use formal analysis techniques, in particular model-checking, to detect emergent patterns of human behaviours that may lead to erroneous interactions. Finally, we show how model-checking may be used as a supporting tool in cognitive psychology to formally verify the correctness and completeness of behavioral theories developed from empirical studies.