School of Computing Science

Staff Profiles

Professor Michael Harrison



Michael is Emeritus Professor and Senior Research Investigator at Newcastle and research fellow at QMUL (funded to work on the analysis of medical devices). He  is a visiting researcher at the University of Minho, Portugal. His research focuses on the systematic analysis of the functional behaviour of interactive systems using a combination of model checking and automated theorem proving techniques. 


Most of my research is concerned with modelling and analysis of devices.

Modelling and systematic analysis of interactive systems

Current research on this topic includes exploring mechanisms for proving properties of specifications of interactive behaviour using model checkers [Campos & Harrison, 2001, 2003] and theorem provers [Harrison, Campos, Masci, 2015]. Some of this work focuses on the IVY tool developed by Jose Campos at Braga. which supports the instantiation of standard property templates to a particular model. These templates can be applied systematically to analyse interactive devices [Campos & Harrison, 2008, 2009, 2011] and [Harrison, Campos & Masci, 2013] and the use of information resources to restrict analysis to cognitively plausible paths [Doherty, Campos & Harrison, 2008,  Campos, Doherty and Harrison, 2014, Harrison, Campos, Silva & Curzon, 2016]. Much of the research now uses the PVS theorem prover. This allows the analysis of larger models.

This research has been funded by a half time research fellowship at QMUL ( in the context of medical instruments. More recent research has considered the complementary role of model checking and theorem proving in the analysis of interactive devices, see for example [Masci et al. 2013].  Most of my work involves collaboration with Campos and Masci at the University of Minho in Braga although I have also developed an analysis as part of a safety case, with the Royal Victoria Infirmary at Newcastle, for a neonatal dialysis machine.

Modelling and analysing flows, with particular focus on ubicomp systems
This is work I would like to do and am currently searching for suitable data. It concerns the use of process algebra techniques to model flow and function is large-scale systems. I have done some preliminary working using these techniques to model human aspects of ubiquitous systems with the aim of enabling a larger scale analysis of the properties of implicit actions that can take place within a physical environment augmented by technology [Silva et al, 2014, Campos et al 2017]. I am particularly interested in quantitative measures that might relate to notions of experience (for example frustration). This work has involved collaboration with Massink in Pisa and Hillston in Edinburgh developing fluid flow models of smart environments [Massink et al, 2012].

User centred design
This is part of the TACTIC project, developing an application to be used by anaesthetists in Trauma care involving "big bleeds" 



I no longer do any teaching.