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 interactive behaviour using model checkers [Campos & Harrison, 2001, 2003]. Much 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, Dittmar & Harrison, 2010, Campos, Doherty and Harrison, 2014].

This research is progressing as part of 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]. Much of the research now uses the PVS theorem prover. This allows the analysis of larger models. The focus now is predominantly medical systems.

Modelling and analysing flows, with particular focus on ubicomp systems
Here I am concerned with the use of process algebra techniques to model flow and function is large-scale systems. These techniques have been used 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]. 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 physicians in Trauma care involving "big bleeds"