School of Computing

Staff Profiles

Professor Michael Harrison



Michael is Emeritus Professor and Senior Research Investigator at Newcastle. He  is a visiting researcher at the University of Minho, Portugal and honorary professor at Swansea. 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. 

Area of expertiseformal modelling of interactive systems, software safety analysis

Google Scholar: Click here.


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].



I no longer do any teaching.