School of Computing

Publications by Prof Howard Bowman

Also view these in the Kent Academic Repository
Books

    Bowman, Howard and Gomez, Rodolfo (2006) Concurrency Theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems. Springer, London, 459 pp. ISBN 1-85233-895-4.

    Abstract

    Concurrency Theory is a synthesis of one of the major threads of theoretical computer science research focusing on languages and graphical notations for describing collections of simultaneously evolving components that interact through synchronous communication. The main specification notation focused on in this book is LOTOS. An extensive introduction to this particular process calculus is given, highlighting how the approach differs from competitor techniques, such as CCS and CSP. The book covers linear-time semantics, based on traces; branching-time semantics, using both labeled transition systems and refusals; and true concurrency semantics, using (bundle) event structures. In addition, the book discusses communicating automata approaches (both finite and infinite state); how the theory can be generalised to the timed setting; and, finally, the authors generalise the (finite and infinite state) communicating automata notations to yield timed automata and discrete timed automata. This book represents a comprehensive pass through the spectrum of concurrency theory research: From untimed to timed syntax and semantics and process calculi to automata. Researchers and practitioners in the field of concurrency theory, as well as MSc and PhD students, will find the comprehensive coverage in this book essential reading.

    Bowman, Howard and Derrick, John (2001) Formal Methods for Distributed Processing, A Survey of Object-oriented Approaches. Cambridge University Press, Cambridge, UK, 480 pp. ISBN 0-521-77184-6.

    Abstract

    This book presents the current state of the art in the application of formal methods to object-based distributed systems. A major theme of the book is how to formally handle the new requirements arising from OO distributed systems, such as dynamic reconfiguration, encapsulation, subtyping, inheritance and real-time aspects. These may be supported either by enhancing existing notations, such as UML, LOTOS, SDL and Z, or by defining new notations, such as Actors, Pi-calculus and Ambients. The major specification notations and modelling techniques are introduced and compared by leading researchers, in several cases the inventors of the notations. The book also includes a description of approaches to the specification of nonfunctional requirements, which are typically needed in the specification of multimedia systems, and a discussion of security issues.

    Bowman, Howard and Thompson, Simon (1998) A tableau method for interval temporal logic with projection. Springer-Verlag Berlin ISBN 3-540-64406-7.

    Abstract

    This paper introduces a tableau method for propositional interval temporal logic (ITL) [14]. Beyond the usual operators of linear temporal logic, ITL contains sequencing and iterative operators, ';' and proj akin to programming combinators. Central to our approach is a normal form for the formulas of ITL, particularly ';' and proj, in terms of the 'O' operator of the logic.

    Blair, Gordon S. and Blair, Lynne and Bowman, Howard et al. (1997) Formal Specification of Distributed Multimedia Systems. University College London Press, 352 pp. ISBN 1-85728-677-4PB.

    Abstract

    The work reported in this book was carried out as part of the EPSRC/DTI sponsored Tempo Project at Lancaster University (in collaboration with BT labs). The aim of the Tempo Project was to investigate formal specification and associated verification techniques to support the development of distributed multimedia systems. The book describes the state of the art in distibuted multimedia computing, highlights requirements for the formal specification and verification of such systems, reviews the available formal specification notations and then, in the light of perceived limitations of the existing approaches, presents a new framework for formal specification of distributed multimedia systems. This framework uses LOTOS to describe the functional behaviour of systems and a real-time temporal logic, called QTL, to describe the non-functional properties.

Articles

    Bowman, Howard and Filetti, Marco and Alsufyani, Abdulmajeed et al. (2014) Countering Countermeasures: Detecting Identity Lies by Detecting Conscious Breakthrough. PLoS ONE, 9 (3). pp. e90595. ISSN 1932-6203.

    Abstract

    One major drawback of deception detection is its vulnerability to countermeasures, whereby participants wilfully modulate their physiological or neurophysiological response to critical guilt-determining stimuli. One reason for this vulnerability is that stimuli are usually presented slowly. This allows enough time to consciously apply countermeasures, once the role of stimuli is determined. However, by increasing presentation speed, stimuli can be placed on the fringe of awareness, rendering it hard to perceive those that have not been previously identified, hindering the possibility to employ countermeasures. We tested an identity deception detector by presenting first names in Rapid Serial Visual Presentation and instructing participants to lie about their own identity. We also instructed participants to apply a series of countermeasures. The method proved resilient, remaining effective at detecting deception under all countermeasures.

    Bowman, Howard and Filetti, Marco and Janssen, Dirk P. et al. (2013) Subliminal Salience Search Illustrated: EEG Identity and Deception Detection on the Fringe of Awareness. PLoS ONE, 8 (1). pp. 1-21. ISSN 1932-6203.

    Abstract

    We propose a novel deception detection system based on Rapid Serial Visual Presentation (RSVP). One motivation for the new method is to present stimuli on the fringe of awareness, such that it is more difficult for deceivers to confound the deception test using countermeasures. The proposed system is able to detect identity deception (by using the first names of participants) with a 100% hit rate (at an alpha level of 0.05). To achieve this, we extended the classic Event-Related Potential (ERP) techniques (such as peak-to-peak) by applying Randomisation, a form of Monte Carlo resampling, which we used to detect deception at an individual level. In order to make the deployment of the system simple and rapid, we utilised data from three electrodes only: Fz, Cz and Pz. We then combined data from the three electrodes using Fisher's method so that each participant was assigned a single p-value, which represents the combined probability that a specific participant was being deceptive. We also present subliminal salience search as a general method to determine what participants find salient by detecting breakthrough into conscious awareness using EEG.

    Bowman, Howard and Filetti, Marco and Wyble, Brad et al. (2013) Attention is more than prediction precision [Commentary on target article]. Behavioral and Brain Sciences, 36 (3). pp. 206-208. ISSN 0140-525X.

    Abstract

    A cornerstone of the target article is that, in a predictive coding framework, attention can be modelled by weighting prediction error with a measure of precision. We argue that this is not a complete explanation, especially in the light of ERP (event-related potentials) data showing large evoked responses for frequently presented target stimuli, which thus are predicted.

    Chennu, Srivas and Alsufyani, Abdulmajeed and Filetti, Marco et al. (2013) The cost of space independence in P300-BCI spellers. Journal of NeuroEngineering and Rehabilitation, 10 (82). pp. 1-13. ISSN 1743-0003.

    Abstract

    Background: Though non-invasive EEG-based Brain Computer Interfaces (BCI) have been researched extensively over the last two decades, most designs require control of spatial attention and/or gaze on the part of the user. Methods: In healthy adults, we compared the offline performance of a space-independent P300-based BCI for spelling words using Rapid Serial Visual Presentation (RSVP), to the well-known space-dependent Matrix P300 speller. Results: EEG classifiability with the RSVP speller was as good as with the Matrix speller. While the Matrix speller’s performance was significantly reliant on early, gaze-dependent Visual Evoked Potentials (VEPs), the RSVP speller depended only on the space-independent P300b. However, there was a cost to true spatial independence: the RSVP speller was less efficient in terms of spelling speed. Conclusions: The advantage of space independence in the RSVP speller was concomitant with a marked reduction in spelling efficiency. Nevertheless, with key improvements to the RSVP design, truly space-independent BCIs could approach efficiencies on par with the Matrix speller. With sufficiently high letter spelling rates fused with predictive language modelling, they would be viable for potential applications with patients unable to direct overt visual gaze or covert attentional focus.

    Su, Li and Bowman, Howard and Barnard, Philip (2011) Glancing and then looking: on the role of body, affect, and meaning in cognitive control. Frontiers in Cognition, 2 (348). pp. 182-196.

    Abstract

    In humans, there is a trade-off between the need to respond optimally to the salient environmental stimuli and the need to meet our long-term goals. This implies that a system of salience sensitive control exists, which trades task-directed processing off against monitoring and responding to potentially high salience stimuli that are irrelevant to the current task. Much cognitive control research has attempted to understand these mechanisms using non-affective stimuli. However, recent research has emphasized the importance of emotions, which are a major factor in the prioritization of competing stimuli and in directing attention. While relatively mature theories of cognitive control exist for non-affective settings, exactly how emotions modulate cognitive processes is less well understood. The attentional blink (AB) task is a useful experimental paradigm to reveal the dynamics of both cognitive and affective control in humans. Hence, we have developed the glancelook model, which has replicated a broad profile of data on the semantic AB task and characterized how attentional deployment is modulated by emotion. Taking inspiration from Barnards Interacting Cognitive Subsystems, the model relies on a distinction between two levels of meaning: implicational and propositional, which are supported by two corresponding mental subsystems: the glance and the look respectively. In our model, these two subsystems reflect the central engine of cognitive control and executive function. In particular, the interaction within the central engine dynamically establishes a task filter for salient stimuli using a neurobiologically inspired learning mechanism. In addition, the somatic contribution of emotional effects is modeled by a body-state subsystem. We argue that stimulus-driven interaction among these three subsystems governs the movement of control between them. The model also predicts attenuation effects and fringe awareness during the AB.

    Wyble, Brad and Potter, Mary C. and Bowman, Howard et al. (2011) Attentional Episodes in Visual Perception. Journal of Experimental Psychology: General, 140 (3). pp. 182-196.

    Abstract

    Is ones temporal perception of the world truly as seamless as it appears? This article presents a computationally motivated theory suggesting that visual attention samples information from temporal episodes (episodic simultaneous type/serial token model; Wyble, Bowman, & Nieuwenstein, 2009). Breaks between these episodes are punctuated by periods of suppressed attention, better known as the attentional blink (Raymond, Shapiro, & Arnell, 1992). We test predictions from this model and demonstrate that participants were able to report more letters from a sequence of 4 targets presented in a dense temporal cluster than from a sequence of 4 targets interleaved with nontargets. However, this superior report accuracy comes at a cost in impaired temporal order perception. Further experiments explore the dynamics of multiple episodes and the boundary conditions that trigger episodic breaks. Finally, we contrast the importance of attentional control, limited resources, and memory capacity constructs in the model.

    Craston, Patrick and Wyble, Brad and Chennu, Srivas et al. (2009) The attentional blink reveals serial working memory encoding: Evidence from virtual and human event-related potentials. Journal of Cognitive Neuroscience, 21 (3). pp. 550-566. ISSN 0898-929X.

    Abstract

    Observers often miss a second target (T2) if it follows an identified first target item (T1) within half a second in rapid serial visual presentation (RSVP), a finding termed the attentional blink. If two targets are presented in immediate succession, however, accuracy is excellent (Lag 1 sparing). The resource sharing hypothesis proposes a dynamic distribution of resources over a time span of up to 600 msec during the attentional blink. In contrast, the ST2 model argues that working memory encoding is serial during the attentional blink and that, due to joint consolidation, Lag 1 is the only case where resources are shared. Experiment 1 investigates the P3 ERP component evoked by targets in RSVP. The results suggest that, in this context, P3 amplitude is an indication of bottom.up strength rather than a measure of cognitive resource allocation. Experiment 2, employing a two-target paradigm, suggests that T1 consolidation is not affected by the presentation of T2 during the attentional blink. However, if targets are presented in immediate succession (Lag 1 sparing), they are jointly encoded into working memory. We use the ST2 model's neural network implementation, which replicates a range of behavioral results related to the attentional blink, to generate .virtual ERPs. by summing across activation traces. We compare virtual to human ERPs and show how the results suggest a serial nature of working memory encoding as implied by the ST2 model.

    Chennu, Srivas and Craston, Patrick and Wyble, Brad et al. (2009) Attention Increases the Temporal Precision of Conscious Perception: Verifying the Neural-ST² Model. PLoS Computational Biology, 5 (11). pp. 182-196.

    Abstract

    What role does attention play in ensuring the temporal precision of visual perception? Behavioural studies have investigated feature selection and binding in time using fleeting sequences of stimuli in the Rapid Serial Visual Presentation (RSVP) paradigm, and found that temporal accuracy is reduced when attentional control is diminished. To reduce the efficacy of attentional deployment, these studies have employed the Attentional Blink (AB) phenomenon. In this article, we use electroencephalography (EEG) to directly investigate the temporal dynamics of conscious perception. Specifically, employing a combination of experimental analysis and neural network modelling, we test the hypothesis that the availability of attention reduces temporal jitter in the latency between a target's visual onset and its consolidation into working memory. We perform time-frequency analysis on data from an AB study to compare the EEG trials underlying the P3 ERPs (Event-related Potential) evoked by targets seen outside vs. inside the AB time window. We find visual differences in phase-sorted ERPimages and statistical differences in the variance of the P3 phase distributions. These results argue for increased variation in the latency of conscious perception during the AB. This experimental analysis is complemented by a theoretical exploration of temporal attention and target processing. Using activation traces from the Neural-ST2 model, we generate virtual ERPs and virtual ERPimages. These are compared to their human counterparts to propose an explanation of how target consolidation in the context of the AB influences the temporal variability of selective attention. The AB provides us with a suitable phenomenon with which to investigate the interplay between attention and perception. The combination of experimental and theoretical elucidation in this article contributes to converging evidence for the notion that the AB reflects a reduction in the temporal acuity of selective attention and the timeliness of perception.

    Wyble, Brad and Sharma, Dinkar and Bowman, Howard (2008) Strategic Regulation of Cognitive Control by Emotional Salience: A Neural Network Model. Cognition and Emotion, 22 (6). pp. 1019-1051. ISSN 0269-9931.

    Abstract

    We present a neural network model of stimulus processing, which uses a mechanism of adaptive attentional control to regulate the moment to moment deployment of attention according to both the demands of the current task, and the demands of emotionally salient information. This mechanism allows negative emotional information to reduce cognitive control to aid in the detection of threats, which produces a momentary withdrawal from the current task set to allow unbiased processing of available information. The combination of cognitive and emotional regulation of task set allows this model to address inter-trial aspects of emotional interference in colour naming. In particular, we focus on the nature of the emotional interference in colour naming (McKenna Sharma, 2004) as well as in word reading (Algom, Chajut, Lev, 2004) and show how this form of interference is functionally distinct from the classic Stroop effect. Our model addresses a range of findings in colour naming and word reading tasks and is informed by recent neuroimaging data concerning the interaction between the anterior cingulate and prefrontal cortices. The model is used to explore the interface between cognition and emotion with a series of predictions, including a qualitative distinction between state and trait forms of anxiety.

    Van Hooff, Johanna C. and Dietz, Kristina Charlotte and Sharma, Dinkar et al. (2008) Neural correlates of intrusion of emotion words in a modified Stroop task. International Journal of Psychophysiology, 67 (1). pp. 23-34. ISSN 0167-8760.

    Abstract

    Behavioural studies have demonstrated that the emotional Stroop task is a valuable tool for investigating emotion-attention interactions in a variety of healthy and clinical populations, showing that participants are typically more distracted by negative stimuli as compared to neutral or positive stimuli. The main aim of this study was to find and examine the neural correlates of this greater intrusion from negative emotional stimuli. Reliable reaction time (RT) and event-related potential (ER-P) data were collected from 23 participants who performed a manual emotional Stroop, task with short (40 ins) and long (500 ms) inter-trial intervals. In the short interval condition, participants were found to produce longer RTs for negative than neutral words, suggesting that these stimuli were more difficult to ignore. This RT effect disappeared in the long interval condition, although larger PI amplitudes were found for the negative words. This suggests that differences in early attention allocation may be unrelated to the degree of intrusion at the behavioural level. In addition, a larger negative slow wave around 300-700 ms post-stimulus was observed in the long interval condition, but only for those negative words that produced prolonged RTs as compared to their matched controls. This late and broadly distributed effect is believed to reflect suppression of meaning representations.

    Bowman, Howard and Wyble, Brad and Chennu, Srivas et al. (2008) A Reciprocal Relationship Between Bottom-up Trace Strength and the Attentional Blink Bottleneck: Relating the LC-NE and ST2 Models. Brain Research, 1202. pp. 25-42. ISSN 0006-8993.

    Abstract

    There is considerable current interest in neural modelling of the attentional blink phenomenon. Two prominent models of this task are the Simultaneous Type Serial Token (ST2) model and the Locus Coeruleus Norepinephrine (LC-NE) model. The former of these generates a broad spectrum of behavioural data, while the latter provides a neurophysiologically detailed account. This paper explores the relationship between these two approaches. Specifically, we consider the spectrum of empirical phenomena that the two models generate, particularly emphasizing the need to generate a reciprocal relationship between bottom-up trace strength and the blink bottleneck. Then we discuss the implications of using ST2 token mechanisms in the LC-NE setting.

    Wyble, Brad and Bowman, Howard and Nieuwenstein, Mark (2008) The Attentional Blink provides Episodic Distinctiveness: Sparing at a Cost. Journal of Experimental Psychology: Human Perception and Performance. ISSN 0096-1523.

    Abstract

    The Attentional Blink (Raymond et al 1992) refers to a surprising temporal gap in our ability to see a target if it follows a prior target. Theoretical and computational work has provided a variety of explanations for the blink, but more recent data have challenged these accounts by showing the blink is strongly attenuated when subjects encode entire strings of targets (Nieuwenstein & Potter, 2006, Olivers et al 2007, Kawahara et al 2007) or are distracted (Olivers & Nieuwenstein 2005). In this paper, we describe the Episodic Simultaneous Type Serial Token (eSTST) model of encoding items into working memory as visual tokens. This model is composed of neurobiologically plausible neural elements and suggests that the attentional blink is the result of a mechanism that creates episodically distinct representations within working memory. The model also addresses the phenomenon of repetition blindness and whole report superiority, producing predictions which are supported by experimental work.

    Wyble, Brad and Bowman, Howard and Potter, Mary C. (2008) Categorically Defined Targets Trigger Spatiotemporal Attention. Journal of Experimental Psychology: Human Perception and Performance. ISSN 0096-1523.

    Abstract

    Transient attention to a visually salient cue enhances processing of a subsequent target in the same spatial location between 50 to 150 ms after cue onset (Nakayama & Mackeben, 1989). Do stimuli from a categorically defined target set, such as letters or digits, also generate transient attention? Participants reported digit targets among keyboard symbols in a changing array of 8 items. When one target preceded a second target in the same location at an SOA of 107 ms (but not 213 ms), the second target was reported more often than in a condition in which there was no leading target. When the two targets were at different locations, report of the second target was impaired. With both letters and digits as targets, the enhancement effect was shown not to be due to category priming. Critically, the attentional benefit was present whether or not participants reported the leading target. Transient attention, contingent attentional capture, popout, and lag 1 sparing in the attentional blink may involve a common mechanism for directing processing resources towards salient and task relevant stimuli.

    Su, Li and Bowman, Howard and Barnard, Philip et al. (2008) Process Algebraic Modelling of Attentional Capture and Human Electrophysiology in Reactive Systems. Formal Aspects of Computing. ISSN 0934-5043.

    Abstract

    Previous research has developed a formal methods-based (cognitive-level) model of the Interact- ing Cognitive Subsystems central engine, with which we have simulated attentional capture in the context of Barnard's key-distractor Attentional Blink task. This model captures core aspects of the allocation of human attention over time and as such should be applicable across a range of practical settings when human attentional limitations come into play. In addition, this model simulates human electrophysiological data, such as electroencephalogram recordings, which can be compared to real electrophysiological data recorded from human participants. We have used this model to evaluate the performance trade-os that would arise from varying key parameters and applying either a constructive or a reactive approach to improving in- teractive systems in a stimulus rich environment. A strength of formal methods is that they are abstract and the resulting specications of the operator are general purpose, ensuring that our ndings are broadly applicable. Thus, we argue that new modelling techniques from computer science can also be employed in computational modelling of the mind. These would complement existing techniques, being specically tar- geted at psychological level modelling, in which it is advantageous to directly represent the distribution of control.

    Kalidindi, Kiran and Bowman, Howard (2007) Using e-greedy reinforcement learning methods to further understand ventromedial prefrontal patients' deficits on the Iowa Gambling Task. Neural Networks, 20 (6). pp. 676-689. ISSN 0893-6080.

    Abstract

    An important component of decision making is evaluating the expected result of a choice, using past experience. The way past experience is used to predict future rewards and punishments can have profound effects on decision making. The aim of this study is to further understand the possible role played by the ventromedial prefrontal cortex in decision making, using results from the Iowa Gambling Task (IGT). A number of theories in the literature offer potential explanations for the underlying cause of the deficit(s) found in bilateral ventromedial prefrontal lesion (VMF) patients on the IGT. An errordriven e-greedy reinforcement learning method was found to produce a good match to both human normative and VMF patient groups from a number of studies. The model supports the theory that the VMF patients are less strategic (more explorative), which could be due to a working memory deficit, and are more reactive than healthy controls. This last aspect seems consistent with a myopia for future consequences.

    Bowman, Howard and Wyble, Brad (2007) The Simultaneous Type, Serial Token Model of Temporal Attention and Working Memory. Psychological Review, 114 (1). pp. 38-70. ISSN 0033-295X.

    Abstract

    A detailed description of the Simultaneous Type Serial Token (STST) model is presented. STST is a model of temporal attention and working memory, which encapsulates five principles: 1) Chun and Potter's (1995) 2-stage model; 2) a stage one Salience Filter; 3) Kanwisher's Types-tokens distinction; 4) a Transient Attentional Enhancement; and 5) a mechanism for associating types with tokens called the Binding Pool. We instantiate this theoretical position in a connectionist implementation, called Neural-STST, which we illustrate by modeling temporal attention results, focused on the Attentional Blink (AB). We demonstrate that the STST model explains a spectrum of AB findings. Furthermore, we highlight a number of new temporal attention predictions arising from the STST theory, which we test in a series of behavioral experiments. Finally, we review major AB models and theories, and compare them to STST.

    Bowman, Howard and Gomez, Rodolfo (2006) How to stop time stopping. Formal Aspects of Computing, 18 (4). pp. 459-493. ISSN 0934-5043.

    Abstract

    Zeno-timelocks constitute a challenge for the formal verification of timed automata: they are difficult to detect, and the verification of most properties (e.g., safety) is only correct for timelock-free models. Some time ago, Tripakis proposed a syntactic check on the structure of timed automata: If a certain condition (called strong non-zenoness) is met by all the loops in a given automaton, then zeno-timelocks are guaranteed not to occur. Checking for strong non-zenoness is efficient, and compositional (if all components in a network of automata are strongly non-zeno, then the network is free from zeno-timelocks). Strong non-zenoness, however, is sufficient-only: There exist non-zeno specifications which are not strongly non-zeno. A TCTL formula is known that represents a sufficient-and-necessary condition for non-zenoness; unfortunately, this formula requires a demanding model-checking algorithm, and not all model-checkers are able to express it. In addition, this algorithm provides only limited diagnostic information. Here we propose a number of alternative solutions. First, we show that the compositional application of strong non-zenoness can be weakened: Some networks can be guaranteed to be free from Zeno-timelocks, even if not every component is strongly non-zeno. Secondly, we present new syntactic, sufficient-only conditions that complement strong non-zenoness. Finally, we describe a sufficient-and-necessary condition that only requires a simple form of reachability analysis. Furthermore, our conditions identify the cause of zeno-timelocks directly on the model, in the form of unsafe loops. We also comment on a tool that we have developed, which implements the syntactic checks on Uppaal models. The tool is also able to derive, from those unsafe loops in a given automaton (in general, an Uppaal model representing a product automaton of a given network), the reachability formulas that characterise the occurrence of zeno-timelocks. A modified version of the CSMA/CD protocol is used as a case-study.

    Wyble, Brad and Bowman, Howard (2006) A neural network account of binding discrete items into working memory using a distributed pool of flexible resources. Journal of Vision, 6 (6). pp. 33-33a. ISSN 1534-7362.

    Schlaghecken, Friederike and Bowman, Howard and Eimer, Martin (2006) Dissociating Local and Global Levels of Perceptuo-Motor Control in Masked Priming. Journal of Experimental Psychology: Human Perception and Performance, 32 (3). pp. 618-632. ISSN 0096-1523.

    Abstract

    Masked prime stimuli presented near the threshold of conscious awareness affect responses to subsequent targets. The direction of these priming effects depends on the temporal characteristics of the prime-mask-target sequence. With short prime/mask-target intervals, benefits for compatible trials (primes and targets mapped to the same response) and costs for incompatible trials are observed. This pattern reverses with longer intervals. We argue a) that these effects reflect the initial activation and subsequent self-inhibition of the primed response, and the corresponding inhibition and subsequent disinhibition of the non-primed response, and b) that they are generated at dissociable local (within response channels) and global (between channels) levels of motor control. In two experiments, global-level priming effects were modulated by changing the number of response alternatives, whereas local-level effects remained unaffected. This suggests that low-level motor control mechanisms can be successfully decomposed into separable sub-components, operating at different levels within the motor system.

    Craston, Patrick and Wyble, Brad and Bowman, Howard (2006) An EEG study of masking effects in RSVP [Abstract]. Journal of Vision, 6 (6). pp. 1016-1016. ISSN 1534-7362.

    Abstract

    We present an EEG study that investigates how target items are processed when presented in Rapid Serial Visual Presentation (RSVP). The RSVP task was similar to the well-known Attentional Blink experiment [Chun and Potter, 1995], however, the stream contained only one target. To increase task difficulty, the presentation rate was doubled to 47ms SOA. Half the targets were followed by a blank to test the effects of backward masking. A skeletal task [Ward et al., 1997] allowed study of targets presented without surrounding distractors (except a following mask). Subjects' EEG waves were recorded at 20 electrode sites. The study was motivated by predictions made on the basis of the ST2 model of temporal attention and visual working memory [Wyble and Bowman, 2005] concerning the influence of masking and task difficulty on target processing. In line with our predictions, the following results are observed: We find delayed processing of targets in RSVP streams compared to targets that are presented stand-alone (skeletal). In RSVP streams we do not observe accelerated processing of masked compared to unmasked targets as suggested by Kessler et al. (2005). A categorisation of target letters based on subject performance ('hard' or 'easy') modulates target ERPs, in particular the P3 component. Finally, we investigate the 'all-or-none' issue of conscious perception [Sergent et al., 2005] by correlating subjects' task performance and P3 amplitude using EEG single-trial analysis.

    Bowman, Howard and Schlaghecken, Friederike and Eimer, Martin (2006) A Neural Network Model of Inhibitory Processing in Subliminal Priming. Visual Cognition, 13 (4). pp. 401-480. ISSN 1464-0716(electronic)1350-6285(paper).

    Abstract

    Masked Priming Experiments have revealed a precise set of facilitatory and inhibitory visual-motor control processes. Most notably, inhibitory effects have been identified in which prime-target compatibility induces performance costs and prime-target incompatibility induces performance benefits. We argue that this profile of data is commensurate with an ?emergency braking mechanism?, whereby responses can be retracted as a result of changing sensory evidence. The main contribution of this paper is to provide a neural network based explanation of this phenomenon. This is obtained through the use of feedforward inhibition to implement backward masking, lateral inhibition to implement response competition and opponent processing mechanisms to implement response retraction. Although the model remains simple, it does a very good job of reproducing the available masked priming data. For example, it reproduces a large spectrum of reaction time data across a number of different experimental conditions. Perhaps most notably however, it also reproduces Lateralized Readiness Potentials that have been recorded while subjects perform different conditions. In addition, it provides a concrete set of testable predictions.

    Bowman, Howard and Gomez, Rodolfo and Su, Linying (2005) A tool for the syntactic detection of zeno-timelocks in timed automata. Electronic Notes in Theoretical Computer Science, 139 (1). pp. 25-47. ISSN 1571-0661.

    Abstract

    Timed automata are a very successful notation for specifying and verifying real-time systems, but timelocks can freely arise. These are counter-intuitive situations in which a specifier's description of a component automaton can inadvertently prevent time from passing beyond a certain point, possibly making the entire system stop. In particular, a zeno-timelock represents a situation where infinite computation is performed in a finite period of time. Zeno-timelocks are very hard to detect for real-time model checkers, e.g. UPPAAL and Kronos. We have developed a tool which can take an UPPAAL model as input and return a number of loops which can potentially cause zeno-timelocks. This tool implements an algorithm which refines a static verification approach introduced by Tripakis. We illustrate the use of this tool on a real-life case-study, the CSMA/CD protocol.

    Wyble, Brad and Bowman, Howard (2005) The attentional blink reflects the time course of token binding, computational modeling and empirical data (Abstract). Journal of Vision, 5 (8). pp. 116a-116a. ISSN 1534-7362.

    Abstract

    A previously published computational model of the Attentional Blink (Wyble and Bowman, 2004) has given rise to predictions about the time course of the U-shaped T2 performance curve that is characteristic of the AB. Specifically, we posit that the blink curve is a hallmark of limitations in the temporal resolution of the binding of working memory tokens to types. In our model, lag-1 sparing results from a temporal window approximately 150 msec in length during which multiple items can be bound to the same token. Recovery of the blink occurs when a second token becomes available for binding. In testing these predictions, we have performed two AB experiments. The first experiment compared the shape of AB curves for RSVP streams in the style of Chun and Potter (1995), presented at either 10 or 20 items/sec. If the AB is the result of temporal processes, the shape of the curve should be constant with respect to time. In our data, the blink curves had the same shape with respect to the time lag between T1 and T2, not the number of items. Specifically, in the faster presentation stream, we observed lag-2 sparing, maximal depth at lag 6 and recovery by lag 12. Our second experiment involved presenting subjects with a letter pair for each of T1 and T2. If sparing involves binding T1 and T2 into a single conglomerate token, there should be a high percentage of binding errors at lag 1, in which one element of T1 is swapped with one element of T2. This prediction was confirmed, subjects made many binding errors at lag-1, and returned to baseline levels of error by lag-2. This work details our continuing efforts to use the AB paradigm to explore the temporal structure of working memory. These data support our theoretical position that the AB stems from limitations in the consolidation of working memory tokens. We present these data in the context of a previously published connectionist model of the AB.

    Gomez, Rodolfo and Bowman, Howard (2004) PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic. Journal of Applied Non-Classical Logics, 14 (1-2). pp. 105-148. ISSN 1166-3081.

    Abstract

    Interval Temporal Logic (ITL) is a finite-time linear temporal logic with applications in hardware verification, temporal logic programming and specification of multimedia documents. Due to the logic's non-elementary complexity, efficient ITL-based verification tools have been difficult to develop, even for propositional subsets. MONA is an efficient implementation of an automata-based decision procedure for the logic WS1S. Despite the non-elementary complexity of WS1S, MONA has been successfully applied in problems such as hardware synthesis, protocol verification and theorem proving. Here we consider a rich propositional subset of ITL, PITL, whose expressive power is equivalent to that of WS1S, and in turn to that of regular languages. PITL not only includes operators such as chop, star and projection, but also past operators such as previous, chop in the past and since. We provide an interpretation of PITL formulas in WS1S, which led us to a direct translation from PITL formulas to MONA specifications. We present the tool PITL2MONA as an implementation of such translation. With PITL2MONA acting as a front-end, MONA is used as a decision procedure for PITL. To our knowledge, this is one of the few implementations of a decision procedure for PITL, the first one based on automata, and the only one which handles both projection and past operators. We have tested our implementation on a number of examples; we show in this paper the application of PITL and its MONA-based decision procedure in solutions to the dining-philosophers and a multimedia synchronisation problem, together with some experimental results on these and some other examples.

    Barnard, Philip and Bowman, Howard (2004) Rendering Information Processing Models of Cognition and Affect Computationally Explicit: Distributed Executive Control and the Deployment of Attention. Cognitive Science Quarterly, 3 (3). pp. 297-328. ISSN 1466-6553.

    Abstract

    In this paper we illustrate the potential of process algebra to implement modular mental architectures of wide scope in which control is distributed rather than centralised. Drawing on the Interacting Cognitive Subsystems (ICS) mental architecture, we present an implemented model of the attentional blink effect. The model relies on process exchanges between propositional meaning and a more abstract, implicational level of meaning, at which affect is represented and experienced. We also discuss how the proposed mechanism of buffer movement can, in the context of the ICS architecture, be extended to account for effects of emotional stimuli and brain damage.

    Bryans, Jeremy W. and Bowman, Howard and Derrick, John (2003) Model Checking Stochastic Automata. ACM Transactions on Computational Logic, 4 (4). pp. 452-492. ISSN 1529-3785.

    Abstract

    Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time constraints are crucial to their correct functioning. In order to specify such systems it is necessary to describe that events occur at times given by probability distributions; stochastic automata have emerged as a useful technique by which such systems can be specified and verified.However, stochastic descriptions are very general, in particular they allow the use of general probability distribution functions, and therefore their verification can be complex. In the last few years, model checking has emerged as a useful verification tool for large systems. In this article we describe two model checking algorithms for stochastic automata. These algorithms consider how properties written in a simple probabilistic real-time logic can be checked against a given stochastic automaton.

    Bowman, Howard and Thompson, Simon (2003) A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection. Journal of Logic and Computation, 13 (2). pp. 195-239. ISSN 0955-792X.

    Abstract

    This paper presents a complete axiomatization for propositional interval temporal logic (PITL) with projection. The axiomatization is based on a tableau decision procedure for the logic, which in turn is founded upon a normal form for PITL formulae. The construction of the axiomatization provides a general mechanism for generating axiomatizations thus: given a normal form for a new connective, axioms can be generated for the connective from the tableau construction using that normal form. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

    Bowman, Howard and Cameron, Helen and King, Peter et al. (2003) Mexitl: Multimedia in Executable Interval Temporal Logic. Formal Methods in System Design, 22 (1). pp. 5-38. ISSN 0925-9856.

    Abstract

    This paper explores a formalism for describing a wide class of multimedia document constraints. The formalism is based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical specification example. Then we present the temporal logic formalism that we use. This extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection like operator called filter and a new handling of interval length. A model theory and satisfaction relation is defined for the notation and a specification of the canonical example is presented.

    Bowman, Howard and Steen, Maarten and Boiten, Eerke et al. (2002) A Formal Framework for Viewpoint Consistency. Formal Methods in System Design, 21 (2). pp. 111-166. ISSN 0925-9856.

    Abstract

    Multiple Viewpoint models of system development are becoming increasingly important. Each viewpoint offers a different perspective on the target system and system development involves parallel refinement of the multiple views. Viewpoints related approaches have been considered in a number of different guises by a spectrum of researchers. Our work particularly focuses on the use of viewpoints in Open Distributed Processing (ODP) which is an ISO/ITU standardisation framework. The requirements of viewpoints modelling in ODP are very broad and, hence, demanding. Multiple viewpoints, though, prompt the issue of consistency between viewpoints. This paper describes a very general interpretation of consistency which we argue is broad enough to meet the requirements of consistency in ODP. We present a formal framework for this general interpretation; highlight basic properties of the interpretation and locate restricted classes of consistency. Strategies for checking consistency are also investigated. Throughout we illustrate our theory using the formal description technique LOTOS. Thus, the paper also characterises the nature of and options for consistency checking in LOTOS.

    Bowman, Howard (2001) Formal Methods Elsewhere. Electronic Notes in Theoretical Computer Science, 43. pp. 162-163. ISSN 1571-0661.

    Abstract

    The FM-Elsewhere workshop, co-located with FORTE-PSTV-2000 in Pisa, was a forum for researchers interested in the application of formal methods to virtually any area of research, except communication protocols and software engineering. The talks included in the workshop covered the spectrum of FM-Elsewhere areas. In particular, applications of formal methods to all the following areas were considered, safety analysis of cockpit interfaces; solving games and puzzles using state space exploration techniques; modelling theories of the mind; usability anaylsis of human computer interfaces; formal definition of linguistic systems; and modelling in mechanics and physics.

    Bowman, Howard and Bryans, Jeremy W. and Derrick, John (2001) Analysis of a Multimedia Stream using Stochastic Process Algebra. Computer Journal, 44 (4). pp. 230-245. ISSN 0010-4620.

    Abstract

    It is now well recognised that the next generation of distributed systems will be distributed multimedia systems. Central to multimedia systems is quality of service, which defines the non-functional requirements on the system. In this paper we investigate how stochastic process algebra can be used in order to determine the quality of service properties of distributed multimedia systems. We use a simple multimedia stream as our basic example. We describe it in the Stochastic Process Algebra PEPA and then we analyse whether the stream satisfies a set of quality of service parameters: throughput, end-to-end latency, jitter and error rates.

    Bowman, Howard and Derrick, John and Brinksma, E. (2000) Selected papers from the Second IFIP Int'l Conference on Formal Methods for Open Object Based Distributed Systems, 1997. IEEE Transactions on Software Engineering, 26 (7). pp. 577-578. ISSN 0098-5589.

    Boiten, Eerke and Bowman, Howard and Derrick, John et al. (2000) Viewpoint Consistency in ODP. Computer Networks, 34 (3). pp. 503-537. ISSN 1389-1286.

    Abstract

    Open Distributed Processing (ODP) is a joint ITU/ISO standardisation framework for constructing distributed systems in a multi-vendor environment. Central to the ODP approach is the use of viewpoints for specification and design. Inherent in any viewpoint approach is the need to check and manage the consistency of viewpoints. In previous work we have described techniques for consistency checking, refinement, and translation between viewpoint specifications, in particular for LOTOS and Z/Object-Z. Here we present an overview of our work, motivated by a case study combining these techniques in order to show consistency between viewpoints specified in LOTOS and Object-Z.

    Bowman, Howard and Derrick, John and Brinksma, E. (2000) Guest Editors Introduction: Formal Methods for Object Oriented Distributed Systems. IEEE Transactions on Software Engineering, 26 (7). pp. 577-578.

    Boiten, Eerke and Derrick, John and Bowman, Howard et al. (1999) Constructive consistency checking for partial specification in Z. Science of Computer Programming, 35 (1). pp. 29-75. ISSN 0167-6423.

    Abstract

    Partial specification is a method of specifying complex systems in which the system is described by a collection of specifications, each approaching the system from a different viewpoint. The specification notation Z is often advocated as a suitable language for this style of specification. For collections of partial specifications to be meaningful, they need to be consistent, i.e. they should not impose contradictory requirements. This paper addresses how the consistency between partial specifications in Z can be checked, by constructing unifications, i.e. least common refinements, of viewpoint specifications.

    Bowman, Howard and Boiten, Eerke and Derrick, John et al. (1999) Strategies for consistency checking based on unification. Science of Computer Programming, 33 (3). pp. 261-298. ISSN 0167-6423.

    Abstract

    There is increasing interest in models of system development which use Multiple Viewpoints. Each viewpoint offers a different perspective on the target system and system development involves parallel refinement of the multiple views. Multiple viewpoints though, prompt the issue of consistency between viewpoints. This paper describes an interpretation of consistency which is general enough to meet the requirements of consistency for very general viewpoints models. Furthermore, the paper investigates strategies for checking this consistency definition. Particular emphasis is placed on mechanisms to obtain global consistency (between an arbitrary number of viewpoints) from a series of binary consistency checks. The consistency checking strategies we develop are illustrated using the formal description technique LOTOS.

    Derrick, John and Boiten, Eerke and Bowman, Howard et al. (1999) Viewpoints and consistency: translating LOTOS to Object-z. Computer Standards and Interfaces, 21 (3). pp. 251-272. ISSN 0920-5489.

    Abstract

    This paper presents a translation between the formal description technique LOTOS and the object-oriented specification language Object-Z. The need for such a translation lies in the use of formal methods in viewpoint specification, and in particular in the Open Distributed Processing standard. The use of viewpoints as a set of partial interlocking specifications brings an obligation to check the consistency of these partial specifications, and to do so we need to relate specifications written in differing languages. The work presented here aims to support the consistency checking of viewpoints written using formal methods by defining a translation from LOTOS to Object-Z. A LOTOS specification describes both an ADT component and a behavioural model, the former is translated into the Z type system, and the behavioural specification is translated into a collection of Object-Z classes where we relate LOTOS actions to operations in the Object-Z specification. A case study is presented which illustrates the translation and consistency checking techniques discussed in the paper.

    Bowman, Howard and Faconti, Giorgio (1999) Analysing Cognitive Behaviour using LOTOS and Mexitl. Formal Aspects of Computing, 11 (2). pp. 132-159.

    Abstract

    We argue that cognitive models should be used in analysing the usability of multi-modal human computer interfaces and further, that formal methods can be advantageously applied to such analysis. In pursuing this objective we specify the Interacting Cognitive Subsystems model formally using the process calculus LOTOS and then we verify that it satisfies certain behavioural goals formulated in the interval temporal logic Mexitl.

    Derrick, John and Boiten, Eerke and Bowman, Howard et al. (1998) Specifying and Refining Internal Operations in Z. Formal Aspects of Computing, 10 (2). pp. 125-159. ISSN 0934-5043(Print)1433-299X(Online).

    Abstract

    Abstract An important aspect in the specification of distributed systems is the role of the internal (or unobservable) operation. Such operations are not part of the interface to the environment (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. In this paper we are interested in the use of the formal specification notation Z for the description of distributed systems. Various conventions have been employed to model internal operations when specifying such systems in Z. If internal operations are distinguished in the specification notation, then refinement needs to deal with internal operations in appropriate ways. Using an example of a telecommunications protocol we show that standard Z refinement is inappropriate for refining a system when internal operations are specified explicitly. We present a generalization of Z refinement, called weak refinement, which treats internal operations differently from observable operations when refining a system. We discuss the role of internal operations in a Z specification, and in particular whether an equivalent specification not containing internal operations can be found. The nature of divergence through livelock is also discussed. Keywords: Z; Refinement; Distributed Systems; Internal Operations; Process Algebras; Concurrency.

    Bowman, Howard and Faconti, Giorgio and Katoen, J-P. et al. (1998) Automatic Verification of a Lip Synchronisation Protocol using UPPAAL. Formal Aspects of Computing, 10 (5-6). pp. 550-575. ISSN 1433-299X.

    Abstract

    We present the formal specification and verification of a lip synchronisation algorithm using the real-time model checker UPPAAL. A number of specifications of this algorithm can be found in the literature, but this is the first automatic verification. We take a published specification of the algorithm, code it up in the UPPAAL timed automata notation and then verify whether the algorithm satisfies the key properties of jitter and skew. The verification reveals some flaws in the algorithm. In particular, it shows that for certain sound and video streams the algorithm can timelock before reaching a prescribed error state.

    Bowman, Howard (1998) A LOTOS Based Tutorial on Formal Methods for Object Oriented Distributed Systems. New Generation Computing, 16 (4). pp. 343-372. ISSN 0288-3635.

    Abstract

    The majority of formal methods for distributed systems have their origins in the 1980's and were targeted at the early generations of distributed systems. However, modern distributed systems have new features not found in the early systems, e.g. they are object-oriented, have mobile components, are time sensitive and are constructed according to advanced system development architectures, e.g. viewpoints models. A major topic of current research is thus, how to enhance the existing formal techniques in order to support these new features. This paper gives a tutorial level review of this research area. We particularly focus on the process algebra LOTOS and consider how the technique can be reconciled with these new features.

    Charles, Nathan and Bowman, Howard and Thompson, Simon (1997) From ACT-ONE to Miranda, a Translation Experiment. Computer Standards and Interfaces, 19 (1). pp. 31-49. ISSN 0920-5489.

    Abstract

    It is now almost universally acknowledged that the data language ACT-ONE associated with the formal description technique LOTOS is inappropriate for the purpose of OSI formal description. In response to this the LOTOS restandardisation activity plans to replace ACT-ONE with a functional language. Thus, compatibility between ACT-ONE and the replacement data language becomes an issue. In response to this, we present an experimental investigation of backward compatibility between ACT-ONE and the new LOTOS data language. Specifically, we investigate translating ACT-ONE data types into the functional language Miranda. Miranda has been chosen as it is a widely used functional programming language and it is close in form to the anticipated new data language. This work serves as a ``verification of concept'' for translating ACT-ONE to the E-LOTOS data language. It identifies the bounds on embedding ACT-ONE in a functional data language. In particular, it indicates what can be translated and what cannot be translated. In addition, the paper reveals pertinent issues which can inform the E-LOTOS work. For example, which constructs are needed in E-LOTOS in order to support the class of data type specifications typically made in the LOTOS setting? We conclude with a number of specific recommendations for the E-LOTOS data language.

    Bowman, Howard and Derrick, John and Linington, Peter F. et al. (1996) Cross-viewpoint consistency in open distributed processing. Software Engineering Journal, 11 (1). pp. 44-57. ISSN 0268-6961.

    Abstract

    The paper discusses the use of viewpoints in the ODP (Open Distributed Processing) standardisation initiative. The ODP reference model is a new framework, going beyond OSI (Open Systems Interconnection). Multiple viewpoints are used to specify complex ODP systems. Consistency of viewpoint specifications is clearly a central issue. In addition, formal techniques have an increasingly significant role within ODP, and so mechanisms are needed that support consistency checking of formal specifications. An overview is provided of the ODP reference model and the use of viewpoints within it, before discussing consistency within ODP and how it can be realised using formal notations. Consistency checking is illustrated using the LOTOS formal description technique.

    Bowman, Howard and Derrick, John and Linington, Peter F. et al. (1995) FDTs for ODP. Computer Standards and Interfaces, 17 (5-6). pp. 457-479. ISSN 0920-5489.

    Abstract

    This paper discusses the use and integration of formal techniques into the Open Distributed Processing (ODP) standardization initiative. The ODP reference model is a natural progression from OSI. Multiple viewpoints are used to specify complex ODP systems. Formal methods are playing an increasing role within ODP. We provide an overview of the ODP reference model, before discussing the ODP requirements on FDTs, and the role such techniques play. Finally we discuss the use of formalisms in the central problem of maintaining cross viewpoint consistency.

    Blair, Lynne and Blair, Gordon S. and Bowman, Howard et al. (1995) Formal Specification and Verification of Multimedia Systems in Open Distributed Processing. Computer Standards and Interfaces, 17 (5-6). pp. 413-436. ISSN 0920-5489.

    Abstract

    The field of distributed systems is now entering a stage of maturity with work focusing on standards for Open Distributed Processing (ODP). However, it is still important that standardization remains responsive to new technological demands such as the emergence of distributed multimedia computing. This paper focuses on the likely impact of multimedia computing on formal description within ODP. In particular, a framework is proposed for the formal specification and verification of quality of service and more general real-time concerns in distributed multimedia systems. This framework exhibits a separation of concerns between the specification of behaviour and requirements and also between the specification of abstract behaviour and real-time concerns. The usefulness of this framework is demonstrated by the development of an approach based on LOTOS together with a real-time temporal logic, QTL.

Book Sections

    Bowman, Howard and Li, Su (2011) Cognition, Concurrency Theory and Reverberations in the Brain: in Search of a Calculus of Communicating (Recurrent) Neural Systems. In: Voronkov, Andrei and Korovina, Margarita Higher-Order Workshop on Automated Runtime Verification and Debugging, EasyChair Proceedings, Festschrift celebrating Howard Barringer's 60th Birthday. EasyChair. ISBN xxxxx.

    Abstract

    We consider whether techniques from concurrency theory can be applied in the area of Cognitive Neuroscience. We focus on two potential applications. The first of these explores structural decomposition, which is effectively assumed by the localisation of function metaphor that so dominates current Cognitive Neuroscience. We take concurrency theory methods, especially Process Calculi, as canonical illustrations of system description notations that support structural decomposition and, in particular, encapsulation of behaviour. We argue that carrying these behavioural and notational properties over to the Cognitive Neuroscience setting is difficult, since neural networks (the modelling method of choice) are not naturally encapsulable. Our second application presents work on verifying stability properties of neural network learning algorithms using model checking. We thereby present evidence that a particular learning algorithm, the Generalised Recirculation algorithm, exhibits an especially severe form of instability, whereby it forgets what it has learnt, while continuing to be trained on the same pattern set.

    Bowman, Howard and Su, Li and Wyble, Brad et al. (2009) Salience Sensitive Control, Temporal Attention and Stimulus-Rich Reactive Interfaces. In: Roda, Claudia Human Attention in Digital Environments. Cambridge University Press.

    Wyble, Brad and Sharma, Dinkar and Bowman, Howard (2005) Modelling the slow emotional stroop effect: Suppression of cognitive control. In: Cangelosi, Angelo and Bugmann, Guido Modelling Language, Cognition and Action. Proceedings of the Ninth Neural Computation and Psychology Workshop, University of Plymouth, UK 8 - 10 September 2004. Progress in Neural Processing (16). World Scientific Publishing Company Pte Ltd, Singapore, pp. 291-300. ISBN 981-256-324-5.

    Abstract

    Our connectionist model provides a theoretical explanation for the existence of slow and fast emotional Stroop effects, and depicts them as independent but interacting phenomena. We build upon previous modelling work by Cohen et a] (1990) and Botvinick et al (2001) among others, and incorporate data that suggest a functional division of the Anterior Cingulate Cortex (ACC) into Cognitive and Affective Divisions. This work suggests that slow emotional Stroop effects are caused by activation of the affective portion of the ACC, which inhibits the Cognitive division, reducing top-down cognitive control on the subsequent trial.

    Bowman, Howard and Derrick, John (2001) Issues in Formal Methods (chapter 3). In: Bowman, Howard and Derrick, John Formal Methods for Distributed Processing, A Survey of Object-oriented Approaches. Cambridge University Press, Cambridge, UK, pp. 18-35. ISBN 0-521-77184-6.

    Abstract

    The previous two chapters of this book discuss the construction of distributed systems and highlight some of the challenges that they pose. The central problem that these chapters leave is, of course, how to enhance reliability in the context of distribution. For those interested in a formal approach, this gives rise to a number of requirements on both the theoretical framework and particular engineering approaches. In this chapter we draw on some of the themes introduced in Chapters 1 and 2 to discuss implications on the use of formal methods for the specification of distributed systems.

    Bowman, Howard and Derrick, John (2001) Viewpoints Modelling. In: Bowman, Howard and Derrick, John Formal Methods for Distributed Processing, A Survey of Object-oriented Approaches. Cambridge University Press, Cambridge, UK, pp. 451-475. ISBN 0-521-77184-6.

    Abstract

    This final chapter of the book, discusses the theme of architecture by looking at an ODP viewpoints modelling case study. The purpose of the case study is to illustrate viewpoints and show how formal methods can be used in modelling and analysing them. In doing so we illustrate how different languages can be used in different viewpoints and introduce cross-viewpoint consistency and its checking.

Conference Items

    Bowman, Howard and Wyble, Brad and Chennu, Srivas et al. (2011) Fortunate Conjunctions Revived: Feature Binding with the 2f-ST2 Model. In: Proceedings of the 33rd Annual Conference of the Cognitive Science Society.

    Abstract

    Temporal feature binding in vision refers to the process by which features of objects presented one after the other at the same spatial location are correctly bound together. In this paper, we describe a computational model of putative neural mechanisms that would produce this behaviour. These simulations highlight the role of transient attentional enhancement in mediating the temporal binding of features into working memory. This model builds upon previous approaches, and explains a range of behavioural findings relating to the patterns of illusory conjunctions observed in experiments. Further, it provides a parsimonious account of a counter-intuitive pattern of reaction time data.

    Abstract

    Abstract. In previous work, we have developed a Glance-Look model, which has replicated a broad profile of data on the semantic Attentional Blink (AB) task and characterized how attention deployment is modulated by emotion. The model relies on a distinction between two levels of meaning: implicational and propositional, which are supported by two corresponding mental subsystems. The somatic contribution of emotional effects is modeled by an additional body-state subsystem. The interaction among these three subsystems enables attention to oscillate between them. Using this model, we have predicted the pattern of conscious perception during the AB and the changes of awareness when emotional or other task irrelevant processing occurs. We provide a specific account of the interaction between attention, emotion and consciousness. In particular, the dynamics of two modes of attending to meaning (implicational being more distributed and propositional being evaluative and specific) give rise to fringe awareness.

    Abstract

    Mirror effects â??- simultaneous increases in recognition accuracy for old and new items in a given condition

    Chennu, Srivas and Craston, Patrick and Wyble, Brad et al. (2009) The influence of target discriminability on the time course of attentional selection. In: Proceedings of the 31th Annual Conference of the Cognitive Science Society.

    Abstract

    A wealth of neurophysiological data has demonstrated that visual attention can selectively enhance target representations early in the visual processing pathway. In conjunction, behavioural evidence tells us that the extent to which irrelevant items interfere with target processing depends on their featural similarity to the target. In this context, how does target discriminability influence temporal selection? We present results from an electrophysiology study that addresses this question by investigating the time course of the neural processes involved in target selection as target distinctiveness is varied. The results suggest that, in line with previous findings, making discrimination harder reduces the accuracy of target identification. We find that there are significant differences in the perceptual processing of the target in the two conditions, as indexed by early visual ERPs and the P3 ERP. We ground this and previous empirical evidence within a theoretical framework for understanding the mechanism of attentional selection represented in the ST2 model, a neural network model of temporal attention and working memory. By simulating both experimental conditions, we show that the model provides a convincing explanation of the pattern of experimental results, in addition to informing questions about the nature and time course of attentional selection.

    Bowman, Howard and Craston, Patrick and Chennu, Srivas et al. (2009) The delayed consolidation hypothesis of all-or-none conscious perception during the attentional blink, applying the ST2 framework. In: Proceedings of the 31st Annual Conference of the Cognitive Science Society.

    Abstract

    There is evidence that conscious perception during the attentional blink is all-or-none, which contrasts with the finding of a continuum of perceptual strength in masking experiments. This seems to reveal the underlying representation of strength that can be found in the brain in the absence of attentional enhancement. We provide electrophysiological support for this all-or-none theory. Then, using principles from the ST2 model of temporal attention and working memory, we show how this all-or-none pattern can be explained by the delayed attentional enhancement/target consolidation that is known to arise during the attentional blink.

    Chennu, Srivas and Craston, Patrick and Wyble, Brad et al. (2008) Transient Attentional Enhancement during the Attentional Blink: ERP correlates of the ST2 model. In: From Associations to Rules: Connectionist Models of Behavior and Cognition.

    Abstract

    There has been considerable recent interest in the identification of neural correlates of the Attentional Blink (AB), and the development of neurally explicit computational models. A prominent example is the Simultaneous Type Serial Token (ST2) model, which suggests that when the visual system detects a task-relevant item, a spatially specific Transient Attentional Enhancement (TAE), called the blaster, is triggered. This paper reports on our investigations into EEG activity during the AB, and a hypothesized correlation between the blaster and the N2pc ERP component. Specifically, we demonstrate that the temporal firing pattern of the blaster in the model matches the N2pc component in human ERP recordings, for targets that are seen and missed inside and outside the attentional blink window. Such a correlation between a computational account of the AB and ERP data provides useful insights into the processes underlying selectivity in temporal attention.

    Dietz, Kristina Charlotte and Bowman, Howard and Van Hooff, Johanna C. (2008) Towards a competitive learning model of mirror effects in yes/no recognition memory tests. In: Connectionist models of behaviour and cognition II.

    Abstract

    Manipulations of encoding strength and stimulus class can lead to a simultaneous increase in hits and decrease in false alarms for a given condition in a yes/no recognition memory test. Based on signal detection theory, the strength-based `mirror effect' is thought to involve a shift in response criterion/threshold (Type I), whereas the stimulus class effect derives from a specific ordering of the memory strength signals for presented items (Type II). We implemented both suggested mechanisms in a simple, competitive feed-forward neural network model with a learning rule related to Bayesian inference. In a single-process approach to recognition, the underlying decision axis as well as the response criteria/thresholds were derived from network activation. Initial results replicated findings in the literature and are a first step towards a more neurally explicit model of mirror effects in recognition memory tests.

    Sharma, Dinkar and Wyble, Brad and Bowman, Howard (2007) Modulation of Cognitive Control by Negative Affect. Experimental Verification of a Connectionist Model of the Emotional Stroop. In: Experimental Psychology Society conference, 4-7 July 2007, Edinburgh. (unpublished)

    Gomez, Rodolfo and Bowman, Howard (2007) Efficient Detection of Zeno Runs in Timed Automata. In: 5th International Conference FORMATS 2007 (Formal Modelling and Analysis of Timed Systems), October 2007, Salzburg, Austria.

    Abstract

    Zeno runs, where infinitely many actions occur in finite time, may inadvertently arise in timed automata specifications. Zeno runs may compromise the reliability of formal verification, and few model-checkers provide the means to deal with them: this usually takes the form of liveness checks, which are computationally expensive. As an alternative, we describe here an efficient static analysis to assert absence of Zeno runs on Uppaal networks; this is based on Tripakis's strong non-Zenoness property, and identifies all loops in the automata graphs where Zeno runs may possibly occur. If such unsafe loops are found, we show how to derive an abstract network that over-approximates the loop behaviour. Then, liveness checks may assert absence of Zeno runs in the original network, by exploring the reduced state space of the abstract network. Experiments show that this combined approach may be much more efficient than running liveness checks on the original network.

    Su, Li and Bowman, Howard and Barnard, Philip (2007) Performance of Reactive Interfaces in Stimulus Rich Environments, Applying Formal Methods and Cognitive Frameworks. In: UNSPECIFIED Elsevier pp. 95-111.

    Abstract

    Previous research has developed a formal methods-based (cognitive-level) model of the Interacting Cognitive Subsystems central engine, with which we have simulated attentional capture in the context of Barnard's key-distractor Attentional Blink task. This model captures core aspects of the allocation of human attention over time and as such should be applicable across a range of practical settings when human attentional limitations come into play. Thus, we have used this model to evaluate the performance trade-os that would arise from varying key parameters in Stimulus Rich Reactive Interfaces. A strength of formal methods is that they are abstract and thus, the resulting specications of the operator are general purpose, ensuring that our ndings are broadly applicable.

    Su, Li and Bowman, Howard and Barnard, Philip (2007) Attentional capture by meaning: A multi-level modelling study. In: 29th Annual meeting of the cognitive science society (CogSci 2007), August 1-4, 2007, Nashville, Tennessee.

    Abstract

    We present a computational study of attentional capture by meaning, based on Barnard et al's key-distractor attentional blink task. We highlight a sequence of models, from an abstract black-box to a structurally detailed white-box model. Each of these models reproduces the major findings from the key-distractor blink task. We argue that such multi-level modelling gives greater confidence in the theoretical position encapsulated by these models.

    Abstract

    Somatic marker theory proposes that body states act as a valence associated with potential choices based on prior outcomes; and thus aid decision-making. The main supporting evidence for this theory arose from clinical interviews of subjects with ventromedial prefrontal cortex (VMF) lesions and their performance on the Iowa Gambling Task (IGT). VMF patient behaviour has been described as myopia about future consequences. The aim of this paper is to investigate the implications of this description using an abstract simulation of the neural mechanisms that could underlie decision-making in this type of reinforcement learning task.

    Su, Li and Bowman, Howard and Wyble, Brad (2005) Symbolic Encoding of Neural Networks using Communicating Automata with Applications to Verification of Neural Network Based Controllers. In: Nineteenth International Joint Conference on Artificial Intelligence, 30 July - 5 August 2005, Edinburgh, Scotland.

    Abstract

    This paper illustrates a way for applying formal methods techniques to specifying and verifying neural networks, with applications in the area of neural network based controllers. Formal methods have some of the characteristics of symbolic models. We describe a communicating automata [Bowman and Gomez, 2005] model of neural networks, where the standard Backpropagation (BP) algorithm [Rumelhart et al., 1986] is applied. Then we undertake a verification of this model using the model checker Uppaal [Behrmann et al., 2004], in order to predict the performance of the learning process. We discuss broad issues of integrating symbolic techniques with complex neural systems. We also argue that symbolic verifications may give theoretically well-founded ways to evaluate and justify neural learning systems.

    Wyble, Brad and Bowman, Howard (2005) Computational and Experimental Evaluation of the Attentional Blink: Testing the Simultaneous Type Serial Token Model. In: CogSci 2005, XXVII Annual Conference of the Cognitive Science Society, 21-23 July 2005, Stresa, Italy.

    Abstract

    A reduced version of the Simultaneous Type Serial Token Model is presented. This model embraces two theories of temporal attention: Chun and Potter's two-stage theory and Kanwisher's types-tokens theory. We explain the proposed model and show how it reproduces key data from the Attentional Blink phenomenon. In addition, we verify experimentally predictions arising from the model.

    Kalidindi, Kiran and Bowman, Howard and Wyble, Brad (2005) A consideration of decision-making, motivation and emotions within Dual Process theory: supporting evidence from Somatic-Marker theory and simulations of the Iowa Gambling task. In: AISB’05: Social Intelligence and Interaction in Animals, Robots and Agents, 12-15 April 2005, Hatfield, United Kingdom.

    Abstract

    For many years there have been lay people, philosophers and scientists who have made the distinction between affect and cold cognition. This paper examines the potential value of this dichotomy in relation to understanding ventromedial lesion (VMF) patients behaviour in general and on the Iowa Gambling Task (IGT). We use a combination of dual-process and somatic-marker theories and infer-ences based on simulations of normal controls and VMF patients on the IGT.

    Bowman, Howard and Wyble, Brad (2005) Computational Modelling of the Attentional Blink. In: Proceedings of the Neural Computation and Psychology Workshop.

    Abstract

    This paper describes a computational model of the Attentional Blink constructed using the dual-stage model proposed by [1] and also incorporating a token based account of working memory [2]. This model reproduces data from a number of blink paradigms and makes predictions that lag-1 sparing is temporal and not sequential in origin. A further prediction is that enhancing the distinctiveness of T2 can impair T1 performance and also provoke order inversions of T1 and T2. Experiments from our lab examined the validity of these predictions. Implications and results are discussed.

    Wyble, Brad and Bowman, Howard (2004) The Attentional Blink at 20 items/sec, Model Prediction and Empirical Validation of Lag-2 Sparing. In: Proceedings of the International Conference on Cognitive Modelling, JUL 30-AUG 01, 2004, Carnegie Mellon Univ, Pittsburgh, PA,.

    Bowman, Howard and Wyble, Brad and Barnard, Philip (2004) Towards a Neural Network Model of the Attentional Blink. In: Proceedings of the Eighth Neural Computation and Psychology Workshop, Connectionist Models of Cognition and Perception II, Aug 28-30, 2003, Univ Kent Canterbury, Kent, England.

    Abstract

    One of the most prominent experimental paradigms for investigating the deployment of attention over time is the Attentional Blink (AB). Although there is now a great deal known about it, computational modeling of the AB remains only lightly explored. This paper responds to this limitation by proposing a prototype neural network model of the blink. A central aspect of which is a realization of the concept of consolidation into working memory, which is at the heart of the majority of current explanations of the blink.

    Gomez, Rodolfo and Bowman, Howard (2003) Discrete Timed Automata and MONA: Description, Specification and Verification of a Multimedia Stream. In: Konig, H. and Heiner, M. and Wolisz, A. LNCS, 2767 (2767). Springer, Berlin, Germany pp. 177-192. ISBN 3-540-20175-0.

    Abstract

    MONA implements an efficient decision procedure for the weak second-order logic WS1S, and has already been applied in many non-trivial problems. Among these, we follow on from the work of Smith and Klarlund on the verification of a sliding-window protocol. This paper extends the scope of MONA to the verification of time-dependent protocols. We present Discrete Timed Automata (DTA) as a suitable formalism to specify and verify such protocols. In this paper our case study will be the specification and verification of a multimedia stream. DTA are as much influenced by IO Automata (syntactically) as they are by Timed Automata (semantically). A composition strategy is given to combine a set of synchronising automata, resulting in a product automaton over which safety properties can be verified. Invariance proofs are then performed inductively on the automaton structure. MONA supports the mechanical verification of invariance proofs.

    Bowman, Howard and Barnard, Philip (2003) Towards a Neural Network Model of the Attentional Blink (Abstract). In: Proceedings of Seventh International Conference on Cognitive and Neural Systems, May 2003, May 2003., Boston University, May 2003..

    Abstract

    A set of experiments that employ rapid serial visual presentation have clarified the time course of selective attention by identifying what has come to be called the attentional blink. Many theoretical explanations of the phenomenon and associated informal models have been advanced. However, until recently, no formal computational model had been developed. This paper responds to this limitation by constructing a prototype neural network model of the blink.

    Bowman, Howard and Schlaghecken, Friederike and Eimer, Martin (2002) Neural Network Modelling of Inhibition in Visuo-Motor Control. In: Proceedings of the Seventh Neural Computation and Psychology Workshop: Connectionist Models of Cognition and Perception, September 2002.

    Abstract

    Masked priming experiments have shown that perceptuo-motor linkages can be made below the threshold of conscious experience. Notable amongst these experiments is work by Eimer and Schlaghecken that has shown that negative compatibility effects can be obtained, whereby behavioural costs are incurred when prime and target are compatible. Negative compatibility is suggestive of inhibitory mechanisms; a theory that is supported by lateralized readiness recordings of motor cortex activation. This paper develops a neural network model of masked priming that yields such negative compatibility. The key mechanisms that facilitate this outcome are (lateral inhibition based) competition between response alternatives and (opponent processing based) threshold gated direct response suppression. The main result of our model is the generation of response readiness profiles commensurate with the lateralized readiness potentials recorded from humans.

    Bowman, Howard and Schlaghecken, Friederike and Eimer, Martin (2002) A Connectionist Model of Inhibition in Masked Priming (abstract). In: Proceedings of Sixth International Conference on Cognitive and Neural Systems, May 30th - June 1st, 2002, May 30th to June 1st 2002, Boston, Massachussetts.

    Abstract

    A key question that has come to dominate a large body of research on perception to action coupling is the role that consciousness plays in such binding. In fact, there is now considerable evidence that visual stimuli can affect response tendencies even when the stimuli are not consciously perceived. Furthermore, there is also now evidence that subliminally presented stimuli can induce inhibitory effects. It is argued that this inhibitory reversal implements an emergency breaking mechanism - once the evidence for a response is removed (as accrues from mask presentation) the corresponding motor action is suppressed. These results prompt consideration of the computational mechanism that underlies such an inhibitory reversal. Our proposal is that the effect arises from the interplay of response competition (as implemented by lateral inhibition) and a threshold gated direct suppression of strongly activated response nodes. The latter of these is implemented using dedicated opponent processing circuits, Here we present a neural networks-based implementation of these principles, the behaviour of which has a good fit to the available data.

    Bowman, Howard (2001) Time and Action Lock Freedom Properties of Timed Automata. In: Formal Techniques for Networked and Distributed Systems.

    Abstract

    Time and action locks can arise freely in timed automata specification. We review techniques for avoiding the occurrence of timelocks, based on the Timed Automata with Deadlines framework. Then we present a notion of parallel composition which preserves action lock freeness, in the sense that, if any component automaton is action lock free, then the composition will also be action lock free.

    Bryans, Jeremy W. and Blair, Lynne and Bowman, Howard et al. (2000) Specification and Analysis of Automata-based Designs. In: Grieskamp, Wolfgang and Stanten, Thomas and Stoddart, Bill Lecture Notes in Comuter Science, 1945. Springer pp. 176-193. ISBN 3-540-41196-8.

    Abstract

    One of the results of research into formal system specification has been the large number of notations which have been developed. Of these notations, automata have emerged as a promising vehicle for the specification, and particularly the analysis, of systems. This is especially so when the systems under consideration include timing requirements, and timed automata model such systems as a finite set of states with timed transitions between them. However, not all specifications involve deterministic timing, and stochastic automata can be used in these circumstances. In this paper we consider both timed and stochastic automata, and demonstrate how they can be used in the same design. We will also consider what analysis of the specification can then be performed. In particular, we will describe how to translate stochastic to timed automata, and look at two approaches to model checking the stochastic components of an integrated design.

    Bowman, Howard and Bryans, Jeremy W. and Derrick, John (2000) Towards Stochastic Model Checking with Generalised Distributions. In: UKPEW 2000, 16th United Kingdom Performance Engineering Workshop, July 24-25, 2000, Durham Univ. uk,.

    Bowman, Howard and Faconti, Giorgio and Massink, M. (2000) Towards Integrated Cognitive and Interface Analysis. In: Proceedings of Formal Methods Elsewhere 2000, Pisa, Italy.

    Abstract

    Using cognitive architectures to analyse the usability of human-computer interfaces is an extensively investigated strategy. A particularly powerful way to perform such analysis is through syndetic modelling, where both the interface and the chosen cognitive model are described in the same specification framework; allowing the combined behaviour of the two to be analysed. This paper proposes LOTOS as a syndetic modelling language. We highlight four reasons why syndetic modelling is so difficult and show how the LOTOS notation addresses each of these four reasons.

    Steen, Maarten and Derrick, John and Boiten, Eerke et al. (1999) Consistency of partial process specifications. In: 7th International Conference on Algebraic Methodology and Software Technology (AMAST 98), Jan 04-08, 1999, Amazonia, Brazil.

    Abstract

    The structuring of the specification and development of distributed systems according to viewpoints, as advocated by the Reference Model for Open Distributed Processing, raises the question of when such viewpoint specifications may be considered consistent with one another. In this paper, we analyse the notion of consistency in the context of formal process specification. It turns out that different notions of correctness give rise to different consistency relations. Each notion of consistency is formally characterised and placed in a spectrum of consistency relations. An example illustrates the use of these relations for consistency checking.

    Bowman, Howard (1999) Modelling Concurrent Cognitive Architectures Using Process Calculi. In: European Conference on Cognitive Science 1999, 27th-30th October 1999, Siena, Italy.

    Abstract

    Theories of concurrent systems have been extensively investigated in the computer science domain. However, these theories are very general in nature and hence, we would argue, are applicable to many disciplines in which concurrency arises. Furthermore, a number of existing theories of cognitive science are concurrent in nature. Thus, we investigate the application of a (process calculi based) concurrency theory to modelling Interacting Cognitive Subsystems, which is such a (concurrent) cognitive theory. Then we consider the capabilities of the cognitive system to perform combinations of speech and gesture in multi-modal human computer interaction.

    Bowman, Howard (1999) Modelling Timeouts without Timelocks. In: UNSPECIFIED Lecture Notes in Computer Science, 1601. Springer-Verlag pp. 334-354.

    Abstract

    We address the issue of modelling a simple timeout in timed automata. We argue that expression of the timeout in the UPPAAL timed automata model is unsatisfactory since when composed with a component behaviour, the timeout can generate timelocks. In response we consider an alternative timed automata framework - timed automata with deadlines. This framework has the property that timelocks cannot be created when composing automata in parallel. We explore a number of different options for reformulating the timeout in this framework and then we relate them.

    Bowman, Howard and Derrick, John (1999) A Junction between State Based and Behavioural Specification. In: Formal Methods for Open Object-based Distributed Systems.

    Abstract

    Two of the dominant paradigms for formally describing and analysing OO distributed systems are state based specification, e.g. Object-Z, and behavioural specification, e.g. process algebra. The style of specification embodied by the two paradigms is highly contrasting. With state based techniques the data state is explicitly defined while the temporal ordering of operations is left implicit, in contrast in behavioural techniques, no explicit data state definition is given while the temporal ordering of action offers is focused on. However, in order to support sophisticated software engineering principles, e.g. multi-paradigm specification, viewpoints modelling and subtyping, there is now considerable interest in developing strategies for relating state based and behavioural specification paradigms. This paper serves two purposes - firstly, it reviews the existing body of work on relating these two specification paradigms and secondly, it presents some new results on the topic. In particular, we present a testing characterisation of downward simulation, which is the standard state based refinement relation and is also closely related to subtyping. Central to this characterisation is giving a behavioural interpretation to the meaning of state based operations outside their pre-conditions.

    Bowman, Howard and Bryans, Jeremy W. and Derrick, John (1998) Analysis of a Multimedia Stream using Stochastic Process Algebra. In: Sixth International Workshop on Process Algebras and Performance Modelling, 1998.

    Abstract

    It is now well recognised that the next generation of distributed systems will be distributed multimedia systems. Central to multimedia systems is quality of service, which defines the non-functional requirements on the system. In this paper we investigate how stochastic process algebra can be used in order to determine the quality of service properties of distributed multimedia systems. We use a simple multimedia stream as our basic example. We describe it in the Stochastic Process Algebra PEPA and then we analyse whether the stream satisfies a set of quality of service parameters: throughput, end-to-end latency, jitter and error rates.

    Bowman, Howard and Faconti, Giorgio and Massink, M. (1998) Specification and Verification of Media Constraints using UPPAAL. In: 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSV-IS 98, Jun 03-05, 1998, Abington, England,.

    Abstract

    We present the formal specification and verification of a multimedia stream. The stream is described in a timed automata notation. We verify that the stream satisfies certain quality of service properties, in particular, throughput and end-to-end latency. The verification tool used is the real-time model checker UPPAAL.

    Cameron, Helen and King, Peter and Bowman, Howard et al. (1998) Synchronization in Multimedia Documents. In: Andre, Jacques Lecture Notes In Computer Science, 1357. Springer pp. 355-369. ISBN 3-540-64298-6.

    Abstract

    This paper presents a taxonomy of possible synchronization relationships between pairs of items in multimedia documents. Several existing approaches to the synchronization of entire items are reviewed. We then discuss classes of synchronization based upon dynamic events or conditions occurring within media items and their internal structure. We present a taxonomy of seventy-two possible such relations, which are illustrated by numerous examples and which are formalized in the authors' temporal logic notation, Mexitl. The ideas are then applied to provide a description of the lip-synchronization problem.

    Bowman, Howard and Thompson, Simon (1998) A Tableaux Method for Interval Temporal Logic with Projection. In: UNSPECIFIED Lecture Notes In Computer Science, 1397 (1397). Springer-Verlag pp. 108-123. ISBN 3-540-64406-7.

    Abstract

    Tableau Methods have been extensively investigated for standard (infinite) temporal logics and there has been some tableau work in the interval temporal logic setting. However, this work has not considered the important projection operator. This paper responds to this deficiency by defining just such a tableau algorithm which handles the projection operator.

    Bowman, Howard and Faconti, Giorgio and Katoen, J-P. et al. (1998) Automatic Verification of a Lip-Synchronisation Algorithm Using UPPAAL - Extended Version. In: FMICS'98, Third Internatinoal Workshop on Formal Methods for Industrial Crtical Systems.

    Abstract

    We present the formal specification and verification of a lip synchronisation algorithm using the real-time model checker UPPAAL. A number of specifications of this algorithm can be found in the literature, but this is the first automatic verification. We take a published specification of the algorithm, code it up in the UPPAAL timed automata notation and then verify whether the algorithm satisfies the key properties of jitter and skew. The verification reveals some flaws in the algorithm. In particular, it shows that for certain sound and video streams the algorithm can timelock before reaching a prescribed error state.

    Bowman, Howard and Katoen, J-P. (1998) A True Concurrency Semantics for ET-LOTOS. In: CSD'98 International Conference on Application of Concurrency to System Design, Mar 23-26, 1998, Fukushima, Japan.

    Abstract

    One of the central objectives of the LOTOS restandardisation activity is to define an enhanced LOTOS language which supports real-time specification. The timed extension is based upon a timed LOTOS proposal ET-LOTOS. This paper defines a (branching-time) non-interleaving semantics for ET-LOTOS without data. As a denotational model a suitable timed extension of Langerak's bundle event structures is used. For guarded recursive processes we show the consistency between our non-interleaving semantics and the ET-LOTOS interleaving semantics. Since our semantical model does not have an explicit notion of the passage of time (as opposed to the interleaving semantics) we are able to handle unguarded recursion and Zeno-behaviours in a perspicuous way.

    Bowman, Howard and Derrick, John (1997) Extending LOTOS with time: A true concurrency perspective. In: 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software (ARTS 97), May 21-23, 1997, Palma De Mallorca, Spain.

    Abstract

    An ongoing restandardisation activity is currently extending the OSI specification language LOTOS with quantitative time. We give an alternative perspective on this activity. We highlight a very simple but expressive timed LOTOS enhancement which is based on time intervals. The main point at which we depart from the standard approach to extending LOTOS with time, is that we employ a true concurrency semantics. We present a semantics based on a time extended bundle event structures. We give a full semantics for relating our timed LOTOS to timed bundle event structures. A fixed point theory is defined and finally, we describe how urgency can be supported in the language.

    Steen, Maarten and Bowman, Howard and Derrick, John et al. (1997) Disjunction of LOTOS specifications. In: Mizuno, Tadanori and Shiratori, Norio and Higashino, Teruo et al. Chapman & Hall, Osaka, Japan pp. 177-192. ISBN 0-412-82060-9.

    Abstract

    LOTOS is a formal specification language, designed for the precise description of open distributed systems and protocols. The definition of, so called, implementation relations has made it possible also to use LOTOS as a specification technique for the design of such systems. These LOTOS based specification techniques usually (ab)use non-determinism to achieve implementation freedom. Unfortunately, this is unsatisfactory when specifying non-deterministic processes. We, therefore, propose to extend LOTOS with a disjunction operator in order to achieve more implementation freedom while maintaining the possibility to describe non-deterministic processes. In contrast with similar proposals we maintain the operational semantics.

    Boiten, Eerke and Bowman, Howard and Derrick, John et al. (1997) Viewpoint consistency in Z and LOTOS: A case study.

    Abstract

    Specification by viewpoints is advocated as a suitable method of specifying complex systems. Each viewpoint describes the envisaged system from a particular perspective, using concepts and specification languages best suited for that perspective. Inherent in any viewpoint approach is the need to check or manage the consistency of viewpoints and to show that the different viewpoints do not impose contradictory requirements. In previous work we have described a range of techniques for consistency checking, refinement, and translation between viewpoint specifications, in particular for the languages LOTOS and Z. These two languages are advocated in a particular viewpoint model, viz. that of the Open Distributed Processing (ODP) reference model. In this paper we present a case study which demonstrates how all these techniques can be combined in order to show consistency between a viewpoint specified in LOTOS and one specified in Z. Keywords: Viewpoints; Consistency; Z; LOTOS; ODP.

    Bowman, Howard and Cameron, Helen and King, Peter et al. (1997) Specification and Prototyping of Structured Multimedia Documents using Interval Temporal Logic. In: International Conference on Temporal Logic.

    Abstract

    This paper explores a formalism for describing a wide class of multimedia document constraints. The formalism is based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical document example. Then we present the temporal logic formalism that we use. This formalism extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection-like operator called filter and a new handling of interval length. A model theory and satisfaction relation is defined for the notation and a specification of the canonical example is presented.

    Boiten, Eerke and Derrick, John and Bowman, Howard et al. (1997) Coupling schemas: data refinement and view(point)composition. In: Northern formal methods, 1997; Jul, Ilkley.

    Abstract

    We define the notion of a coupling schema in Z, and describe the role it plays in data refinement, view composition, and viewpoint unification. In each case coupling schemas relate several state schemas. In data refinement they occur as retrieve relations (abstraction schemas). In specification by views, coupling schemas provide a link between the various views. For viewpoint specification, coupling schemas are closely related to correspondence relations between state schemas in the viewpoints. Simple properties of coupling schemas (e.g. totality, functionality, and consistency) are shown to have important consequences in the techniques listed, and to be very useful for exhibiting the relations between these techniques. It turns out that views and viewpoints can both be seen as variations on, or even as generalisations of, data refinement.

    Bowman, Howard and Briscoe-Smith, C. and Derrick, John et al. (1997) On Behavioural Subtyping in LOTOS. In: Bowman, Howard and Derrick, John Chapman and Hall pp. 335-351. ISBN 0-412-82040-4.

    Abstract

    We consider how the OO notion of subtyping relates to LOTOS testing theory. In particular, we investigate which of the standard LOTOS preorders is a suitable instantiation of behavioural subtyping and argue that each of the main preorders, trace preorder, trace extension, reduction and extension, is in some way deficient. Then, in the light of pre and post condition based models of OO subtyping, we re-work the basic interpretation applied to LOTOS behaviour descriptions. We argue that this re-interpretation enables reduction to be used as an instantiation of behavioural subtyping.

    Derrick, John and Boiten, Eerke and Bowman, Howard et al. (1997) Translating LOTOS to Object-Z. In: 2nd BCS-FACS Northern Formal Methods Workshop : Proceedings of the 2nd BCS-FACS Northern Formal Methods Workshop, 14-15 July, 1997, Ilkley, U. K..

    Abstract

    This paper presents a translation between the formal description technique LOTOS and the object-oriented specification language Object-Z. The need for such a translation lies in the use of formal methods in viewpoint specification, and in particular in the Open Distributed Processing standard. The use of viewpoints as a set of partial interlocking specifications brings an obligation to check the consistency of these partial specifications, and to do so we need to relate specifications written in differing languages. The work presented here supports the consistency checking of viewpoints written using formal methods by defining a translation from full LOTOS to Object-Z. A common semantic model is provided for the languages, and we verify the translation with respect to this model. The translation is illustrated with a small example. http://www1.bcs.org.uk/DocsRepository/02700/2749/derrick.pdf on BCS website; see also /pubs/1999/954/.

    Bowman, Howard and Derrick, John (1997) Extending LOTOS with Time: True Concurrency Perspective. In: Bertran, Miquel and Rus, Teodor Lecture Notes in Computer Science, 1231. Springer-Verlag pp. 382-399. ISBN 3-540-63010-4.

    Abstract

    An ongoing restandardisation activity is currently extending the OSI specification language LOTOS with quantitative time. We give an alternative perspective on this activity. We highlight a very simple but expressive timed LOTOS enhancement which is based on time intervals. The main point at which we depart from the standard approach to extending LOTOS with time, is that we employ a true concurrency semantics. We present a semantics based on time extended bundle event structures. We give a full semantics for relating our timed LOTOS to timed bundle event structures. A fixed point theory is defined and finally, we describe how urgency can be supported in the language.

    Derrick, John and Boiten, Eerke and Bowman, Howard et al. (1997) Weak refinement in Z. In: Bowen, Jonathan P. and Hinchey, Michael G. and Till, David Lecture Notes in Computer Science, 1212. Springer-Verlag, Reading pp. 369-388. ISBN 3-540-62717-0.

    Abstract

    An important aspect in the specification of distributed systems is the role of the internal (or unobservable) operation. Such operations are not part of the user interface (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. Various conventions have been employed to model internal operations when specifying distributed systems in Z. If internal operations are distinguished in the specification notation, then refinement needs to deal with internal operations in appropriate ways. However, in the presence of internal operations, standard Z refinement leads to undesirable implementations. In this paper we present a generalization of Z refinement, called weak refinement, which treats internal operations differently from observable operations when refining a system. We illustrate some of the properties of weak refinement through a specification of a telecommunications protocol. Keywords Refinement; Distributed Systems; Internal Operations; Process Algebras; Concurrency.

    Boiten, Eerke and Bowman, Howard and Derrick, John et al. (1996) Issues in multiparadigm viewpoint specification.

    Abstract

    This paper discusses the issues of specification style and refinement that arise in connection with viewpoint modelling. In particular, we consider the support needed in order to deal with viewpoints at different levels of abstraction. The motivation for this work arises from the use of viewpoints in distributed systems design, in particular the Open Distributed Processing standard. Full proceedings of the workshop it was presented at can be found on WWW: A. Finkelstein and G. Spanoudakis (eds.): http://web.soi.city.ac.uk/homes/gespan/VPFSE.html, ACM SIGSOFT Foundations of Software Engineering 4, 1996.

    Derrick, John and Bowman, Howard and Boiten, Eerke et al. (1996) Comparing LOTOS and Z refinement relations.

    Abstract

    This paper compares the LOTOS and Z refinement relations. The motivation for such a comparison is the use of multiple viewpoints for specifying complex systems defined by the reference model of the Open Distributed Processing (ODP) standardization initiative. The ODP architectural semantics describes the application of formal description techniques (FDTs) to the specification of ODP systems. Of the available FDTs, Z is likely to be used for at least the information, and possibly other, viewpoints, whilst LOTOS is a strong candidate for use in the computational viewpoint. Mechanisms are clearly needed to support the parallel development, and integration of, viewpoints using these FDTs. We compare the LOTOS bisimulation relations and the reduction relations to the Z refinement relation showing that failure-traces refinement corresponds closely to refinement in Z.

    Linington, Peter F. and Derrick, John and Bowman, Howard (1996) The specification and conformance of ODP systems. In: 9th International Workshop on Testing of Communicating Systems.

    Abstract

    Open Distributed Processing (ODP) is a joint standardisation activity of the ISO and ITU. A reference model has been defined which describes an architecture for building open distributed systems. This paper introduces the key aspects of the reference model of open distributed processing, including the ODP conformance framework. We discuss how specific formal techniques are used in the ODP viewpoints, along with the implications for conformance assessment using such techniques. Particular attention is given to the role of consistency in the conformance assessment process. Finally, we review the current work on an ODP conformance testing methodology.

    Bowman, Howard and Boiten, Eerke and Derrick, John et al. (1996) Viewpoint consistency in ODP, a general interpretation.

    Abstract

    Multiple viewpoints are used in Open Distributed Processing (ODP) in order to decompose the complexity inherent in specifying distributed systems. Multiple viewpoints prompt the issue of consistency between viewpoints. The ODP reference model alludes to three different interpretations of consistency. We show that our interpretation, firstly, satisfies all the basic requirements of a definition of consistency and, secondly, can be specialised to any of the three ODP reference model definitions. The generality of our definition will be illustrated through instantiation in the FDT LOTOS.

    Boiten, Eerke and Derrick, John and Bowman, Howard et al. (1996) Consistency and refinement for partial specification in Z.

    Abstract

    This paper discusses theoretical background for the use of Z as a language for partial specification, in particular techniques for checking consistency between viewpoint specifications. The main technique used is unification, i.e. finding a (candidate) least common refinement. The corresponding notion of consistency between specifications turns out to be different from the known notions of consistency for single Z specifications. A key role is played by correspondence relations between the data types used in the various viewpoints. Note: extended version available as /pubs/1999/607/.

    Derrick, John and Boiten, Eerke and Bowman, Howard et al. (1996) Supporting ODP - Translating LOTOS into Z.

    Abstract

    This paper describes a translation of full LOTOS into Z. A common semantic model is defined and the translation is proved correct with respect to the semantics. The motivation for such a translation is the use of multiple viewpoints for specifying complex systems defined by the reference model of the Open Distributed Processing (ODP) standardization initiative. The postscript version available here is an extended version of what was published.

    Boiten, Eerke and Derrick, John and Bowman, Howard et al. (1995) Unification and multiple views of data in Z.

    Abstract

    This paper discusses the unification of Z specifications, in particular specifications that maintain different representations of what is intended to be the same datatype. Essentially this amounts to integrating previously published techniques for combining multiple viewpoints and for combining multiple views. It is shown how the technique proposed in this paper indeed produces unifications, and that it generalises both previous techniques.

    Bowman, Howard and Derrick, John (1995) A True Concurrency Semantics for Quality of Service Specification and Validation. In: MMNet'95, International Conference on Multimedia and Networking.

    Abstract

    This paper considers quality of service specification and validation for distributed multimedia systems. We present a new perspective on the LOTOS/QTL approach to such specification and validation. This approach has been previously presented in the context of a standard interleaving model of concurrency. In this paper we motivate the use of an alternative, truly concurrent, semantic model based on bundle event structures and integrate these semantics into the LOTOS/QTL approach. The applicability of the approach is illustrated with a specification of a multimedia stream.

    Derrick, John and Bowman, Howard and Steen, Maarten (1995) Viewpoints and Objects.

    Abstract

    There have been a number of proposals to split the specification of large and complex systems into a number of inter-related specifications, called viewpoints. Such a model of multiple viewpoints forms the cornerstone of the Open Distributed Processing (ODP) standardisation initiative. We address two of the technical problems concerning the use of formal techniques within multiple viewpoint models: these are unification and consistency checking. We discuss the software engineering implications of using viewpoints, and show that object encapsulation provides the necessary support for such a model. We then consider how this might be supported by using object oriented variants of Z.

    Bowman, Howard and Derrick, John and Steen, Maarten (1995) Some Results on Cross Viewpoint Consistency Checking.

    Abstract

    The ODP multiple viewpoints model prompts the very challenging issue of cross viewpoint consistency. This paper considers definitions of consistency arising from the RM-ODP and relates these in a mathematical framework for consistency checking. We place existing FDTs, in particular LOTOS, into this framework. Then we consider the prospects for viewpoint translation. Our conclusions centre on the relationship between the different definitions of consistency and on the requirements for realistic consistency checking.

    Derrick, John and Bowman, Howard and Steen, Maarten (1995) Maintaining Cross Viewpoint Consistency using Z.

    Abstract

    This paper discusses the use and integration of formal techniques, in particular Z, into the Open Distributed Processing (ODP) standardization initiative. One of the cornerstones of the ODP framework is a model of multiple viewpoints. During the development process it is important to maintain the consistency of different viewpoints of the same ODP specification. In addition, there must be some way to combine specifications from different viewpoints into a single implementation specification. The process of combining two specifications is known as unification. Unification can be used as a method by which to check consistency. This paper describes a mechanism to unify two Z specifications, and hence provide a consistency checking strategy for viewpoints written in Z.

    Bowman, Howard and Derrick, John (1995) Modelling Distributed Systems using Z.

    Abstract

    The ODP development model is a natural progression from OSI. Multiple viewpoints are used to specify complex ODP systems. Formal methods are playing an increasing role within ODP. There are two technical problems concerning the use of formal techniques within ODP which have yet to be addressed: these are unification and consistency checking. We show how Z can be used to provide a solution for both; and hence provide a mechanism for Z to be used properly in the ODP development process.

    Steen, Maarten and Bowman, Howard and Derrick, John (1995) Composition of LOTOS specifications.

    Abstract

    Usually formal methods adopt the traditional waterfall model of system design. New design methodologies, such as Open Distributed Processing and Object Oriented Design, allow for incremental and partial specification. In order to support such design methods, the issues of consistency between specifications and composition of (partial) specification become vital. This paper presents a general framework for dealing with partial specification, which is instantiated for the specification language LOTOS. Necessary and sufficient conditions for consistency to hold between LOTOS specifications are given, and an operational semantics for composition is proposed. Keywords: LOTOS, formal methods, consistency, composition, incremetal specification, refinement.

    Bowman, Howard and Blair, Lynne and Blair, Gordon S. et al. (1994) A Formal Description Technique Supporting Expression of Quality of Service and Media Synchronisation. In: Multimedia Transport and Teleservices, International COST 237 Workshop.

    Abstract

    Formal description techniques have been applied successfully to the fields of communications and distributed systems. We argue, however, that the recent emergence of multimedia computing will have a significant impact on this work. In particular, existing formal description techniques do not satisfactorily model the real-time behaviour exhibited by distributed multimedia systems. This paper considers the impact of multimedia on formal description techniques and proposes an approach in which functional behaviour is expressed in the language LOTOS and non-functional quality of service is expressed in a real-time temporal logic. This dual language approach to formal description is demonstrated through a number of multimedia examples, culminating in the specification of a lip-synchronisation algorithm.

    Bowman, Howard and Derrick, John and Jones, Richard E. (1994) Modelling Garbage Collection Algorithms --- Extend abstract. In: Proceedings of Principles of Distributed Computing'94.

    Abstract

    We show how abstract requirements of garbage collection can be captured using temporal logic. The temporal logic specification can then be used as a basis for process algebra specifications which can involve varying amounts of parallelism. We present two simple CCS specifications as an example, followed by a more complex specification of the cyclic reference counting algorithm. The verification of such algorithms is then briefly discussed.

    Bowman, Howard and Blair, Gordon S. and Blair, Lynne et al. (1993) Time Versus Abstraction In Formal Description. In: FORTE 93 - IFIP 6th International Conference on Formal Description Techniques, Boston, Ma.

    Abstract

    We argue that there is a basic conflict between the incorporation of time and the level of abstraction in formal specification. This conflict is illustrated through the specification of a simple multimedia stream. We propose the principle of separation of timing concerns as a resolution of this conflict and present a dual language notation in order to realise this principle. This notation uses LOTOS to express system behaviour and real-time temporal logic to express timing properties.

Monographs

    Gomez, Rodolfo and Bowman, Howard (2006) Compositional Detection of Zeno Behaviour in Timed Automata. technical_report. Computing Laboratory, CT2 7NF Canterbury, Kent, UK

    Abstract

    The formal specification and verification of real-time systems are difficult tasks, given the complexity of these systems and the safety-critical role they usually play. Timed Automata, and real-time model-checking, have emerged as powerful tools to deal with this problem. However, the specification of urgency in timed automata (essential in most models of interest) may inadvertently cause anomalous behaviours that undermine the reliability of formal verification methods (such as reachability analysis). Zeno runs denote executions which may be arbitrarily fast, i.e., executions where an infinite number of events may occur in a finite period of time. Timelocks denote states where no further divergent execution is possible; i.e., where time cannot pass beyond a certain bound. In general, the verification of safety and liveness properties may be meaningless in models where Zeno runs and timelocks may occur, hence the importance of methods to ensure that models are free from such anomalous behaviours. In previous work, we developed methods to detect Zeno runs and Zeno-timelocks (a particular kind of timelocks) in network of timed automata. Later stages of this analysis derived, from the network's product automaton, reachability formulae that characterise the occurrence of Zeno runs and Zeno-timelocks. Although this simple reachability analysis has a number of advantages over liveness checks (as done in model-checkers such as Uppaal, Kronos and Red), the product automaton is prone to state explosion and so the analysis may not scale well. Here, we refine our previous results by showing that Zeno runs and Zeno timelocks can be characterised by reachability formulae derived from the network's components, i.e., avoiding the product automaton construction.

    Abstract

    Previous research has developed a formal methods-based (cognitive-level) model of the ICS central engine, with which we have simulated attentional capture in the context of Barnard'd key-distractor Attentional Blink task. The same core system would be at work when human operators interact with computer interfaces. Thus, we have used this model to evaluate the performance trade-offs that would arise from varying key parameters in Stimulus Rich Reactive Interfaces (SRRIs). The results of these evaluations are presented in this paper. A strength of formal methods is that they are abstract and thus, the resulting specifications of the operator are general purpose, ensuring that our findings are broadly applicable.

    Wyble, Brad and Bowman, Howard and Craston, Patrick (2006) Attentional Capture in Stimulus Rich Computer Interfaces. technical_report. UKC

    Abstract

    Previous theoretical work has identified a set of attentional mechanisms. This paper explores the practical implications of these mechanisms. Two findings that have particularly inspired this practical work are, 1) the existence of a very rapid (first phase) of attention, called Transient Attentional Enhancement (TAE), which acts within 150ms of stimulus presentation; and 2) that even such rapid attentional deployment is modulated by task set, e.g. it could be initiated by detection of an item in a target category. Such mechanisms have great relevance for the development of Stimulus Rich Reactive Interfaces (SRRIs). In particular, in interfaces with rapidly arriving streams of information, it is important to understand how stimuli capture attention. To explore this issue, this paper presents a prototype SRRI test system. This comprises a central task involving driving through a virtual maze and the presentation of an intermittent stream of competing stimuli of varying levels of salience. Centrally presented arrows are followed in the driving task and the stream of competing stimuli is presented via a head mounted display. The colour relationship between the central arrows and stimuli in the competing stream is varied. How this ''task prescribed'' colour relationship impinges upon attentional capture by stimuli in the competing stream is investigated.

    Abstract

    This paper presents a computational exploration of how meaning modulates temporal attention. This has been explored within the context of Barnard et al's key-distractor Attentional Blink (AB) and proposes a mechanism by which attention is captured by salient meaning. We also explore the applicability of formal methods to the abstract modelling of cognition. Such formal methods enable modelling of an important class of cognitive architectures in which multiple subsystems interact and control is distributed. Most significantly, we have used the formal methods framework to explore the problem of how to relate different levels of abstraction / description in cognitive modelling. Our modelling of Barnard's ICS (Interacting Cognitive Subsystems) architecture illustrates this approach. A major result of our work is the simulation of the key-distractor AB. This simulation is formulated in terms of the interaction between ICS' two central subsystems, which extract implicational and propositional meaning, respectively. Items related to a target category may be interpreted as implicationally salient, even though a later propositional check reveals they are not targets. Such items capture attention, creating a window of time in which the system is vulnerable to missing actual targets. We also explore how changes in semantic salience modulate the key-distractor AB, thereby clarifying the temporal properties of attentional capture by semantic salience.

    Wyble, Brad and Craston, Patrick and Bowman, Howard (2006) Electrophysiological Feedback in Adaptive Human Computer Interfaces. technical_report. UKC

    Abstract

    This paper explores the feasibility of using EEG in the context of Stimulus Rich Reactive Interfaces (SRRI), as a source of feedback on the cognitive state of the user. We have run experiments to evaluate the utility of two potential EEG measures of whether a stimulus has been perceived: 1) reduced EEG power in the alpha band at posterior brain areas and 2) a P3-like positive deflection over parietal areas. Such measures would enable re-presentation of a critical stimulus that has been missed. This paper considers whether, in the context of SRRIs, these measures can be reliably extracted online, i.e. in real-time. To determine this, we have investigated the extent to which online extraction of these measures predicts target report. Our results are positive, particularly with respect to the second approach. we also discuss possible ways in which such a system could be implemented and integrated into a pilot's helmet.

    Li, Su and Bowman, Howard and Barnard, Philip (2006) Emotional Modulation of Temporal Attention, An Approach based upon Distributed Control and Formal Methods. technical_report. UKC

    Abstract

    This paper investigates how emotional salience modulates Barnard et al's key-distractor attentional blink task, enabling us to elucidate the temporal dynamics of attentional capture by emotional stimuli. The research is framed within the context of Barnard's Interacting Cognitive Subsystems (ICS) Architecture. Specifically, we provide a computational model of attentional capture and emotional salience in terms of the interaction between the Implicational, Propositional and Body-State Subsystems that ICS proposes.

    Su, Li and Bowman, Howard and Wyble, Brad (2006) Formal Modeling of Connectionism using Concurrency Theory, an Approach Based on Automata and Model Checking. technical_report. UKC

    Abstract

    This paper illustrates a framework for applying formal methods techniques, which are symbolic in nature, to specifying and verifying neural networks, which are sub-symbolic in nature. The paper describes a communicating automata [Bowman & Gomez, 2006] model of neural networks. We also implement the model using timed automata [Alur & Dill, 1994] and then undertake a verification of these models using the model checker Uppaal [Pettersson, 2000] in order to evaluate the performance of learning algorithms. This paper also presents discussion of a number of broad issues concerning cognitive neuroscience and the debate as to whether symbolic processing or connectionism is a suitable representation of cognitive systems. Additionally, the issue of integrating symbolic techniques, such as formal methods, with complex neural networks is discussed. We then argue that symbolic verifications may give theoretically well-founded ways to evaluate and justify neural learning systems in the field of both theoretical research and real world applications.

    Kalidindi, Kiran and Bowman, Howard and Wyble, Brad (2005) Using e-greedy reinforcement learning methods to further understand ventromedial prefrontal patients' deficits on the Iowa Gambling Task. technical_report., Canterbury, Kent, CT2 7NF, UK

    Abstract

    An important component of decision making is the process of choosing from a set of options. This choice is often based on an evaluation of the potential costs or benefits of selecting an option, its estimated reward value. The foundation for these estimations of costs and benefits is frequently past experience. The way past experience is used to predict future rewards and punishments can have profound effects on choice. Current literature suggests an important role for the orbitofrontal cortex (OFC), in both humans and non-human primates, in representing the reward value of stimuli. The role played by the ventromedial prefrontal cortex (a region which includes the medial OFC) in decision making has previously been tested with the Iowa Gambling Task (IGT), by comparing the performance of patients with bilateral ventromedial prefrontal lesions (VMF) and normal healthy controls (NHCs). A number of theories in the literature offer potential explanations for the underlying cause of the deficit(s) found in VMF patients on the IGT. An empherror-driven ?-greedy reinforcement learning method has been used to model both normative and VMF patient groups from a number of studies, offering support and, more importantly, a deeper understanding of the causes for the `myopia' for future consequences explanation of VMF patients deficits on the IGT.

    Gomez, Rodolfo and Bowman, Howard (2005) Discrete Timed Automata. technical_report. UKC

    Abstract

    MONA implements an efficient decision procedure for the logic WS1S, and has already been applied in many non-trivial problems. Among these, we follow on from previous work done by Smith and Klarlund on the verification of a sliding-window protocol. One of the goals of this paper is to extend the scope of MONA to the verification of time-dependent protocols. We present Discrete Timed Automata (DTA) as a suitable formalism to specify and verify such protocols, and (discrete, infinite-state) real-time systems in general. DTA are as much influenced by IO Automata (syntactically) as they are by Timed Automata (semantically). However, DTA presents a number of distinctive features. Among them, urgency conditions can be directly related to actions, and they are constrained in such a way that time-actionlocks are ruled out by construction. A composition strategy is given to combine a set of synchronising automata, resulting in a product automaton over which safety properties can be verified. Invariance proofs are then performed inductively on the automaton structure, and mechanically assisted by MONA. Therefore, this paper also aims to study benefits and weaknesses of DTA as a real-time formalism, compared with existent frameworks such as Timed IO Automata, TLA+ and Clocked Transition Systems. Our case study will be the specification and verification of a multimedia stream protocol. This is compared to previous work where the formalisation of the protocol is realised in UPPAAL.

    Bowman, Howard and Gomez, Rodolfo and Su, Li (2004) How to stop time stopping (preliminary version). technical_report. University of Kent, Canterbury, Kent, CT2 7NF, UK

    Abstract

    Timed automata are a very successful notation for specifying and verifying real-time systems. One problem of the approach though is that timelocks can freely arise. These are counter-intuitive situations in which a specifier's description of a component automaton can inadvertently prevent time from passing beyond a certain point. This means, in fact, that the entire system stops. We identify a number of different types of timelocks and argue that each type should be treated differently. We distinguish between time-actionlocks and zeno-timelocks and argue that a constructive approach should be applied to preventing the former of these, while an analytical approach should be used to prevent the latter. In accordance with this position, we present a revision of the interpretation of parallel composition in timed automata in order to prevent time-actionlocks. With respect to zeno-timelocks, we present an analytical method to ensure absence of zeno-timelocks which builds upon the notion of strong non-zenoness introduced by Tripakis. We show how Tripakis' results can be extended, broadening the class of timed automata specifications which can be guaranteed to be free from zeno-timelocks. Moreover, we present a tool that we have developed which implements this syntactic verification on UPPAAL-like timed automata specifications. Also, new syntactic properties, in the spirit of strong non-zenoness, are presented which also ensure zeno-timelock freedom. Finally, we illustrate the use of the tool on a real-life case study, the CSMA/CD protocol.

    Gomez, Rodolfo and Bowman, Howard (2003) A MONA-based Decision Procedure for Propositional Interval Temporal Logic. other. Kent University, Vienna, Austria (unpublished)

    Abstract

    Interval Temporal Logic (ITL) is a finite-time linear temporal logic with applications in hardware verifi- cation, temporal logic programming and specification of multimedia documents. Due to the inherently non- elementary complexity of its decision problem, efficient ITL-based verification tools have been difficult to de- velop. We give a new decision procedure for Propositional ITL (PITL) implemented on top of MONA, an efficient automata-based decision procedure for the logic WS1S. Despite the non-elementary complexity of WS1S, MONA has been successfully applied in problems such as hardware synthesis, protocol verification and theorem proving. We have developed a new semantics for PITL based on WS1S formulas, which led us to an easy translation to MONA programs. We have implemented the translation algorithm in C, and the general efficiency of the decision procedure is a direct consequence of the many optimisations included in MONA (e.g. BDDs, DAGification and formula reductions). To our knowledge, this is one of the very few implementations of a decision procedure for PITL with projection, and the first one based on automata.

    Bowman, Howard and Aron, A. and Eimer, E. et al. (2001) A Connectionist Model of Inhibitory Processes in Motor Control and its Application to a Masked Priming Task. technical_report. Computing Laboratory, University of Kent, Canterbury, Canterbury, Kent

    Abstract

    A dominant idea in perceptuo-motor research is that there exists a direct linkage between perception and action. Less clear-cut though is the role that conscious awareness plays in mediating such perceptuo-motor processes. There is though increasing evidence that perceptuo-motor linkages can be made below the threshold of conscious experience. One paradigm which probes this issue is a masked priming paradigm by Eimer and Schlaghecken. The results of this experiment suggest, firstly, that masked primes do modulate responses and, secondly, that inhibition plays a role in the paradigm. This paper responds to these observations by developing a connectionist model of this masked priming task. Key elements of the model are the use of lateral inhibition between response alternatives and opponenet networks in order to generate the required inhibitory reversal.

    Bowman, Howard and Barnard, Philip (2001) Computational Modelling of Distributed Executive Control. technical_report. UKC, Canterbury, Kent, UK

    Abstract

    In this paper we illustrate the potential of process algebra to implement modular mental architectures of wide scope in which control is distributed rather than centralised. Drawing on the Interacting Cognitive Subsystems mental architecture, we present an implemented model of the attentional blink effect which relies on process exchanges between propositional meaning and a more abstract, implicational level of meaning. The key elements that are required in order to obtain the blink are the use of delay-lines to implement time-constrained serial order and also a mechanism for allocating limited attentional resources.

    Akehurst, David H. and Bowman, Howard and Bryans, Jeremy W. et al. (2000) A Manual for a ModelChecker for Stochastic Automata. technical_report. n/a

    Abstract

    This technical report describes a modelchecker for Stochastic Automata, which was built based on the theory described in [BBD00]. The tool is available from: http://www.cs.ukc.ac.uk/people/staff/dha/index.html It accepts a stochastic automaton, a 'timed probabilistic until' formula pattern and a time step parameter. Note that we do not yet allow adversaries, a clock which guards two or more transitions is considered a (run-time) error. Also, we have not yet implemented the full range of the temporal logic in [BBD00]; only the 'timed probabilistic until' queries are allowed, and propositions must be atomic. The algorithm will return one of three results: true, false or undecided. If it returns true, then the automaton models the formula. If it returns false, then the automaton does not model the formula. If it returns undecided, then the algorithm was unable to determine whether the automaton models the formula.

    Bowman, Howard and Thompson, Simon (2000) A Complete Axiomatization of Interval Temporal Logic with Projection. technical_report. University of Kent

    Abstract

    This paper presents a complete axiomatisation for propositional interval temporal logic (PITL) with projection. The axiomatisation is based on a tableau procedure for the logic, which in turn is founded upon a normal form for PITL formluae. The construction of the axiomatisation is modular, in the sense that given a normal form for a new connective, axioms can be generated for the connective from the tableau construction. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

    Bryans, Jeremy W. and Bowman, Howard and Derrick, John (2000) A Model Checking Algorithm for Stochastic Systems. technical_report. University of Kent, Canterbury, Kent

    Abstract

    In this report we present an algorithm for model checking stochastic automata. The algorithm, which is essentially based on discretising time, permits generalised distributions to be used.

    Bowman, Howard (1999) On Time and Action Lock Free Description of Timed Systems. technical_report.

    Abstract

    Time and action locks can arise freely in timed automata specification. While both are error situations, time locks are by far the more serious fault. This is because their occurrence prevents any further evolution of the system. First we investigate techniques for avoiding the occurrence of timelocks. The central aspect of our solution is a redefinition of automata parallel composition based on the Timed Automata with Deadlines Framework of Bornot and Sifakis. Then the second result we present is a notion of parallel composition which preserves action lock freeness. In the sense that, if any component automaton is action lock free, then the composition will also be action lock free.

    Bowman, Howard and Steen, Maarten and Boiten, Eerke et al. (1999) A Formal Framework for Viewpoint Consistency (full version). technical_report., Canterbury, Kent, CT2 7NZ

    Abstract

    Multiple Viewpoint models of system development are becoming increasingly important. Each viewpoint offers a different perspective on the target system and system development involves parallel refinement of the multiple views. Viewpoints related approaches have been considered in a number of different guises by a spectrum of researchers. Our work particularly focuses on the use of viewpoints in Open Distributed Processing (ODP) which is an ISO/ITU standardisation framework. The requirements of viewpoints modelling in ODP are very broad and, hence, demanding. Multiple viewpoints, though, prompt the issue of consistency between viewpoints. This paper describes a very general interpretation of consistency which we argue is broad enough to meet the requirements of consistency in ODP. We present a formal framework for this general interpretation; highlight basic properties of the interpretation and locate restricted classes of consistency. Strategies for checking consistency are also investigated. Throughout we illustrate our theory using the formal description technique LOTOS. Thus, the paper also characterises the nature of and options for consistency checking in LOTOS.

    Bowman, Howard and Faconti, Giorgio and Massink, M. (1999) Towards Integrated Cognitive and Interface Analysis. technical_report.

    Abstract

    Using cognitive architectures to analyse the usability of human-computer interfaces is an extensively investigated strategy. A particularly powerful way to perform such analysis is through syndetic modelling, where both the interface and the chosen cognitive model are described in the same specification framework; allowing the combined behaviour of the two to be analysed. This paper proposes LOTOS as a syndetic modelling language. We highlight four reasons why syndetic modelling is so difficult and show how the LOTOS notation addresses each of the four.

    Bowman, Howard (1998) An Interpretation of Cognitive Theory in Concurrency Theory. technical_report. University of Kent

    Abstract

    Theories of concurrent systems have been extensively investigated in the computer science domain. However, these theories are very general in nature and hence, we would argue, are applicable to many disciplines in which concurrency arises. Furthermore, a number of existing theories of cognitive science are formulated in terms of concurrent subsystems interacting in solving cognitive tasks. In this paper we investigate the application of a (process calculi based) concurrency theory to modelling such a (concurrent) cognitive theory. The cognitive theory chosen is ICS (Interacting Cognitive Subsystems), which we interpret using our process calculus and then we verify some simple behavioural properties of the resulting interpretation. These properties concern the capabilities of the cognitive system to realise deictic reference.

    Bowman, Howard and Thompson, Simon (1997) A Tableau Method for Interval Temporal Logic. technical_report. University of Kent at Canterbury

    Abstract

    In this paper we present a complete tableau method for interval temporal logic including the projection operator. Central to our strategy is the identification of normal forms for all the operators of our logic. In effect, these normal forms give inductive definitions of the ITL operators. Then, in the style of Wolper, we define a tableau decision procedure to check satisfiability of our logic. For simplicity of presentation we work in the propositional setting.

    Bowman, Howard and Cameron, Helen and King, Peter et al. (1997) Mexitl: Multimedia in Executable Interval Temporal Logic. technical_report. University of Kent

    Abstract

    This paper explores a formalism for describing a wide class of multimedia document constraints, based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical specification example. Then we present the temporal logic formalism that we use. This extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection-like operator called filter and a new handling of interval length. A model theory, logic and satisfaction relation are defined for the notation, a specification of the canonical example is presented, and a proof system for the logic is introduced.

    Bowman, Howard and Boiten, Eerke and Derrick, John et al. (1996) Strategies for Consistency Checking, the Choice of Unification. technical_report. UKC, University of Kent, Canterbury, UK

    Abstract

    There is increasing interest in models of system development which use multiple viewpoints. Each viewpoint offers a different perspective on the target system and system development involves parallel refinement of the multiple views. Our work particularly focuses on the use of viewpoints in Open Distributed Processing (ODP) which is an ISO/ITU standardisation framework. Multiple viewpoints, though, prompt the issue of consistency between viewpoints. This paper describes an interpretation of consistency which is general enough to meet the requirements of consistency in ODP. Furthermore, the paper investigates strategies for checking this consistency definition. Particular emphasis is placed on mechanisms to obtain global consistency (between an arbitrary number of viewpoints) from a series of binary consistency checks. The consistency checking strategies we develop are illustrated using the formal description technique LOTOS. Keywords: Viewpoints, Consistency, ODP, Formal Description Techniques, LOTOS.

    Bowman, Howard and Boiten, Eerke and Derrick, John et al. (1995) Strategies for Consistency Checking. technical_report. University of Kent, Computing Laboratory, University of Kent, Canterbury, UK

    Abstract

    Viewpoint models of system development are becoming increasingly important. A major requirement for viewpoints modelling is to be able to check that the multiple viewpoint specifications are consistent with one another. The work presented in this report makes a contribution to this task. Our work is particularly influenced by the viewpoints model used in the ISO standardisation architecture for Open Distributed Processing. This report focuses on the issue of strategies for consistency checking. In particular, it considers how global consistency (between any arbitrary number of viewpoints) can be obtained from binary consistency (between two viewpoints). The report documents a number of different classes of consistency checking, from those that are very poorly behaved to those that are very well behaved. The report is intended as a companion to the work presented in [1] and it should be read in association with this document. In particular, the body of this report is a single chapter which should be viewed as additional to the chapters included in [1]. This report contains complete proofs of all relevant results, even though some of the results are obvious and some of the proofs are trivial. A much compressed version of the report is being submitted for publication. Thus, the main value of this report is as a reference document for readers who require a complete presentation of the technical. [1] E. Boiten, H. Bowman, J. Derrick and M. Steen ''Cross Viewpoint Consistency in Open Distributed Processing (Intra Language Consistency)'', Technical Report, Computing Laboratory, University of Kent at Canterbury, report No. 8-95, 1995. Phone: +44 1227 827913, Fax: 44 1227 762811 Email: H.Bowman,E.A.Boiten,J.Derrick,mwas@ukc.ac.uk.

    Boiten, Eerke and Bowman, Howard and Derrick, John et al. (1995) Cross Viewpoint Consistency in Open Distributed Processing (Intra language consistency). technical_report. UKC, University of Kent, Canterbury, UK

    Abstract

    This document contains the first deliverable of a research project on `Cross Viewpoint Consistency in Open Distributed Processing', carried out at the Computing Laboratory of the University of Kent. Open Distributed Processing (ODP) is recognised as an important area of standardisation activity. The ODP model seeks to provide a standardised architecture for building potentially global distributed systems with components from many vendors. Thus, ODP will realise the open systems ethos in the distributed systems domain. A central concept in ODP is that of a viewpoint. Distributed systems are viewed to be so complex that a process of separation of concerns must be employed when describing such systems. Viewpoints provide such a separation of concerns by presenting five distinct views of a single system; these are the enterprise viewpoint, information viewpoint, computational viewpoint, engineering viewpoint and technology viewpoint. It should be clear that in such viewpoint models it is essential that specifications in different viewpoinmts are related in order to determine whether the muyltiple specifications impose conflicting requirements. The project being reported here responds to this need by investigating how to check that multiple viewpoint specifications are in some sense ''consistent''. The objective of the project is to assess the feasibility of cross viewpoint consistency checking for specifications written in Z and LOTOS. We aim to develop prototype tools and techniques for consistency checking in and between these two specification languages. This deliverable describes the initial phase of the project which has focused on consistency checking methods for individual formalisms. It also contains a fully general framework for consistency checking. Keywords: ODP, LOTOS, Z, consistency, formal methods, distributed systems, software engineering

    Bowman, Howard and Derrick, John (1994) Towards a Formal Model of Consistency in ODP. technical_report. University of Kent, Computing Laboratory, University of Kent, Canterbury, UK

    Abstract

    The ODP (Open Distributed Processing) development model is a natural progression from OSI. Multiple viewpoints are used to specify complex ODP systems. The conformance assessment methodology for ODP defines the relationships between specifications and implementations that must be proved in order that conformance to ODP systems can be asserted. These relationships include transformation, refinement, conformance and consistency. This paper develops a formal interpretation of these concepts. In particular the paper defines a framework for checking the consistency of different specifications of the same ODP system. This framework is essential if FDT's are to be successfully employed in the development of ODP systems. In the second part of the paper, we present examples of consistency checking in both LOTOS and RAISE.

Reviews

    Bowman, Howard and Blair, Gordon S. and Blair, Lynne et al. (1995) Formal description of distributed multimedia systems: An assessment of potential techniques. Computer Communications, 18 (12). pp. 964-977. ISSN 0140-3664.

    Abstract

    The emphasis in distributed multimedia computing has been on developing and building systems, rather than on formally defining the precise behaviour of developed systems. We assess the suitability of a spectrum of formal description techniques for expression of distributed multimedia structures. Then we focus on three particular approaches; extended finite state machines, synchronous languages and process algebras. Representative techniques for each are assessed against multimedia requirements. In particular, we consider to what extent each technique satisfies the real-time requirements of distributed multimedia computing. The conclusions of the paper centre, firstly, on the relative benefits of these specific techniques and, secondly, more broadly, on the limitations of the standard single language based approach for formal description of distributed multimedia systems.

Total publications in KAR: 149 [See all in KAR]

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 31/10/2014