Formal analysis of human-computer interaction using model checking

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.

How checking breeds doubt:reduced performance in a simple working memory task

A paradox of memory research is that repeated checking results in a decrease in memory certainty, memory vividness and confidence [van den Hout, M. A., & Kindt, M. (2003a). Phenomenological validity of an OCD-memory model and the remember/know distinction. Behaviour Research and Therapy, 41, 369–378; van den Hout, M. A., & Kindt, M. (2003b). Repeated checking causes memory distrust. Behaviour Research and Therapy, 41, 301–316]. Although these findings have been mainly attributed to changes in episodic long-term memory, it has been suggested [Shimamura, A. P. (2000). Toward a cognitive neuroscience of metacognition. Consciousness and Cognition, 9, 313–323] that representations in working memory could already suffer from detrimental checking. In two experiments we set out to test this hypothesis by employing a delayed-match-to-sample working memory task. Letters had to be remembered in their correct locations, a task that was designed to engage the episodic short-term buffer of working memory [Baddeley, A. D. (2000). The episodic buffer: a new component in working memory? Trends in Cognitive Sciences, 4, 417–423]. Of most importance, we introduced an intermediate distractor question that was prone to induce frustrating and unnecessary checking on trials where no correct answer was possible. Reaction times and confidence ratings on the actual memory test of these trials confirmed the success of this manipulation. Most importantly, high checkers [cf. VOCI; Thordarson, D. S., Radomsky, A. S., Rachman, S., Shafran, R, Sawchuk, C. N., & Hakstian, A. R. (2004). The Vancouver obsessional compulsive inventory (VOCI). Behaviour Research and Therapy, 42(11), 1289–1314] were less accurate than low checkers when frustrating checking was induced, especially if the experimental context actually emphasized the irrelevance of the misleading question. The clinical relevance of this result was substantiated by means of an extreme groups comparison across the two studies. The findings are discussed in the context of detrimental checking and lack of distractor inhibition as a way of weakening fragile bindings within the episodic short-term buffer of Baddeley's (2000) model. Clinical implications, limitations and future research are considered.

How checking as a cognitive style influences working memory performance

Compulsive checking is known to influence memory, yet there is little consideration of checking as a cognitive style within the typical population. We employed a working memory task where letters had to be remembered in their locations. The key experimental manipulation was to induce repeated checking after encoding by asking about a stimulus that had not been presented. We recorded the effect that such misleading probes had on a subsequent memory test. Participants drawn from the typical population but who scored highly on a checking-scale had poorer memory and less confidence than low scoring individuals. While thoroughness is regarded as a quality, our results indicate that a cognitive style that favours repeated checking does not always lead to the best performance as it can undermine the authenticity of memory traces. This may affect various aspects of everyday life including the work environment and we discuss its implications and possible counter-measures. Copyright © 2010 John Wiley & Sons, Ltd.

Impaired executive functioning in subclinical compulsive checking with ecologically valid stimuli in a working memory task

We previously showed that working memory (WM) performance of subclinical checkers can be affected if they are presented with irrelevant but misleading information during the retention period (Harkin and Kessler, 2009, 2011). The present study differed from our previous research in the three crucial aspects. Firstly, we employed ecologically valid stimuli in form of electrical kitchen appliances on a kitchen countertop in order to address previous criticism of our research with letters in locations as these may not have tapped into the primary concerns of checkers. Secondly, we tested whether these ecological stimuli would allow us to employ a simpler (un-blocked) design while obtaining similarly robust results. Thirdly, in Experiment 2 we improved the measure of confidence as a metacognitive variable by using a quantitative scale (0–100), which indeed revealed more robust effects that were quantitatively related to accuracy of performance. The task in the present study was to memorize four appliances, including their states (on/off), and their locations on the kitchen countertop. Memory accuracy was tested for the states of appliances in Experiment 1, and for their locations in Experiment 2. Intermediate probes were identical in both experiments and were administered during retention on 66.7% of the trials with 50% resolvable and 50% irresolvable/misleading probes. Experiment 1 revealed the efficacy of the employed stimuli by revealing a general impairment of high- compared to low checkers, which confirmed the ecological validity of our stimuli. In Experiment 2 we observed the expected, more differentiated pattern: High checkers were not generally affected in their WM performance (i.e., no general capacity issue); instead they showed a particular impairment in the misleading distractor-probe condition. Also, high checkers’ confidence ratings were indicative of a general impairment in metacognitive functioning. We discuss how specific executive dysfunction and general metacognitive impairment may affect memory traces in the short- and in the long-term.

The role of working memory in compulsive checking and OCD:a systematic classification of 58 experimental findings

Despite the large body of research regarding the role of memory in OCD, the results are described as mixed at best (Hermans et al., 2008). For example, inconsistent findings have been reported with respect to basic capacity, intact verbal, and generally affected visuospatial memory. We suggest that this is due to the traditional pursuit of OCD memory impairment as one of the general capacity and/or domain specificity (visuospatial vs. verbal). In contrast, we conclude from our experiments (i.e., Harkin & Kessler, 2009, 2011; Harkin, Rutherford, & Kessler, 2011) and recent literature (e.g., Greisberg & McKay, 2003) that OCD memory impairment is secondary to executive dysfunction, and more specifically we identify three common factors (EBL: Executive-functioning efficiency, Binding complexity, and memory Load) that we generalize to 58 experimental findings from 46 OCD memory studies. As a result we explain otherwise inconsistent research – e.g., intact vs. deficient verbal memory – that are difficult to reconcile within a capacity or domain specific perspective. We conclude by discussing the relationship between our account and others', which in most cases is complementary rather than contradictory.

Using SAT for Combinational Implementation Checking

The problem of checking whether a system of incompletely specified Boolean functions is implemented by the given combinational circuit is considered. The task is reduced to testing out if two given logical descriptions are equivalent on the domain of one of them having functional indeterminacy. We present a novel SAT-based verification method that is used for testing whether the given circuit satisfies all the conditions represented by the system of incompletely specified Boolean functions.

Approximate Model Checking of Real-Time Systems for Linear Duration Invariants

Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations of the system are often specifiable using Linear Duration Invariants, which is a decidable subclass of Duration Calculus formulas. Various algorithms have been developed to check timed automata or real-time automata for linear duration invariants, but each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented. In this paper, we present an approximate model checking technique based on a genetic algorithm to check real-time automata for linear durration invariants in reasonable times. Genetic algorithm is a good optimization method when a problem needs massive computation and it works particularly well in our case because the fitness function which is derived from the linear duration invariant is linear. ACM Computing Classification System (1998): D.2.4, C.3.

Modelling Provenance of Sensor Data for Food Safety Compliance Checking

Postprint