Skip to main content

Staff Profile

Professor Michael Harrison

Professor

  • Email: michael.harrison@ncl.ac.uk
  • Telephone: +44 191 208 7972
  • Address: School of Computing,
    Urban Sciences Building,
    Newcastle University,
    1 Science Square,
    Newcastle Helix,
    Newcastle upon Tyne,
    NE4 5TG
Background

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 expertise: formal modelling of interactive systems, software safety analysis

Google Scholar: Click here.

Research

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 and tools developed by Paolo Masci. This allows the analysis of larger models.

This research has been funded by a half time research fellowship at QMUL (http://www.chi-med.ac.uk) 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, Harrison et al, 2019, 2021].  Most of the model checking work involves collaboration with Campos 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. The theorem proving work involves collaboration with Masci at the National Institute of Aerospace, USA. A current focus is the analysis of use centred safety requirements in integrated clinical environments.

Current ongoing research is the development of relevant tools to ease the analysis process, see [Campos et al, 2020]


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]. Current research is concerned with the analysis of "big bleed" trauma protocols used by anaesthetists (with Nigel Thomas and our student Ali Alkoradees).


 

Teaching
I no longer do any teaching.
Publications