Â鶹´«Ã½

Skip to main content
School of Computing
Search for something
Search...

Staff Profile

Professor Michael Harrison

Professor

  • Telephone: +44 7889 269739
  • Address: School of Computing,
    Urban Sciences Building,
    Â鶹´«Ã½,
    1 Science Square,
    Â鶹´«Ã½ Helix,
    Â鶹´«Ã½ upon Tyne,
    NE4 5TG
Background

Michael is Emeritus Professor at Â鶹´«Ã½. 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:

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 () 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 Â鶹´«Ã½, 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

  • Articles

    • Harrison MD, Masci P, Campos JC. . Interacting with Computers 2021, 33(1), 55-72.
    • Campos JC, Fayollas C, Harrison MD, Martinie C, Masci P, Palanque P. . ACM Transactions of Computer-Human Interaction 2020, 27(5), 35.
    • Harrison MD, Freitas L, Drinnan M, Campos JC, Masci P, Di Maria C, Whitaker M. . Science of Computer Programming 2019, 175, 17-34.
    • Harrison MD, Masci P, Campos JC. . IEEE Transactions on Software Engineering 2018, 45(8), 802-822.
    • Harrison MD, Masci P, Campos JC, Curzon P. . IEEE Transactions on Human Machine Systems 2017, 47(6), 834-846.
    • Fayollas C, Martinie C, Palanque P, Masci P, Harrison MD, Campos JC, Rodrigues e Silva S. . Electronic Proceedings in Theoretical Computer Science (EPTCS) 2017, 1-19.
    • Campos JC, Abade T, Silva JL, Harrison MD. . Journal of Ambient Intelligence and Humanized Computing 2017, 8(4), 551-566.
    • Campos JC, Sousa M, Alves MCB, Harrison MD. . IEEE Transactions on Human-Machine Systems 2016, 46(2), 303-316.
    • Harrison MD, Campos JC, Masci P. . Innovations in Systems and Software Engineering 2015, 11(2), 95-111.
    • Silva JL, Campos JC, Harrison MD. . International Journal of Human-Computer Studies 2014, 72(5), 488-506.
    • Gomes T, Abade T, Campos JC, Harrison MD, Silva JL. . EAI Endorsed Transactions on Ambient Systems 2014, 14(3), e5.
    • Campos JC, Doherty G, Harrison MD. . International Journal of Human-Computer Studies 2013, 72(3), 284-297.
    • Massink M, Latella D, Bracciali A, Harrison MD, Hillston J. . Formal Aspects of Computing 2012, 24(2), 267-302.
    • Gilroy SW, Harrison MD. . International Journal of Web Engineering and Technology 2008, 4(2), 207-234.
    • Loer K, Harrison MD. . Automated Software Engineering 2006, 13(4), 469-496.
    • Smith SP, Harrison MD. . Reliability Engineering and System Safety 2005, 89(1), 93-104.
    • Campos JC, Harrison MD. . Automated Software Engineering 2001, 8(3-4), 275-310.
    • Willans JS, Harrison MD. . International Journal of Human-Computer Studies 2001, 55(2), 145-165.
    • Doherty GJ, Campos JC, Harrison MD. . Formal Aspects of Computing 2000, 12(4), 260-277.
    • Wright PC, Fields RE, Harrison MD. . Human-Computer Interaction 2000, 15(1), 1-41.
    • Dearden A, Harrison MD, Wright PC. . International Journal of Human-Computer Studies 2000, 52(2), 289-318.
    • Duke DJ, Fields RE, Harrison MD. . Formal Aspects of Computing 1999, 11(2), 107-131.
    • Dearden AM, Harrison MD. . IEEE Aerospace and Electronic Systems Magazine 1997, 12(2), 19-25.
    • McCarthy JC, Healey PGT, Wright PC, Harrison MD. . International Journal of Human-Computer Studies 1997, 47(6), 735-766.
    • Dearden AM, Harrison MD. . International Journal of Human-Computer Studies 1997, 46(1), 151-177.
    • Dearden AM, Harrison MD. . Computer Journal 1997, 40(4), 167-182.
    • Blandford AE, Barnard PJ, Harrison MD. . International Journal of Human-Computer Studies 1995, 43(1), 101-130.
    • Duke DJ, Harrison MD. . Software Engineering Journal 1995, 10(1), 13-20.
    • Duke DJ, Harrison MD. . Software Engineering Journal 1995, 10(1), 3-12.
    • Duke DJ, Harrison MD. . Computer Graphics Forum 1993, 12(3), 25-36.
    • Johnson CW, Harrison MD. . International Journal of Man-Machine Studies 1992, 37(3), 357-385.

  • Book Chapters

    • Campos JC, Harrison MD. . In: Vanderdonckt, J; Palanque, P; Winckler, M, ed. Handbook of Human Computer Interaction. Cham: Springer, 2025, pp.1-28.
    • Harrison MD, Masci PM, Campos JC, Curzon P. . In: Weyers, B; Bowen, J; Dix, A; Palanque, P, ed. The Handbook of Formal Methods in Human-Computer Interaction. Springer International Publishing, 2017, pp.379-403.
    • Harrison MD, Masci P, Campos JC, Curzon P. . In: Huhn, M; Williams, L, ed. Software Engineering in Health Care: proceedings of FHIES 2014 / SEHC 2014. Springer, 2017, pp.113-128.
    • Weyers B, Harrison MD, Bowen J, Palanque P. . In: Weyers, B; Bowen, J; Dix, A; Palanque, P, ed. The Handbook of Formal Methods in Human-Computer Interaction. Springer International Publishing, 2017, pp.89-121.
    • Harrison M, Campos JC, Loer K. . In: Cairns, P., Cox, A.L, ed. Research Methods for Human-Computer Interaction. Cambridge, UK: Cambridge University Press, 2008, pp.88-111.
    • Harrison M, Campos JC, Doherty G, Loer K. . In: Law, E.L-C., Hvannberg, E.T., Cockton, G, ed. Maturing Usability: Quality in Software, Interaction and Value. Berlin: Springer, 2008, pp.56-74.
    • Sujan MA, Smith SP, Harrison MD. . In: Besnard, D., Gacek, C. and Jones, C.B, ed. Structure for Dependability: Computer Based Systems from an Interdisciplinary Perspective. London: Springer-Verlag, 2006, pp.269-287.
    • Loer K, Hildebrandt M, Harrison M. . In: Johnson, C.W., Palanque, P, ed. Human Error, Safety and Systems Development. Boston; London: Kluwer Academic, 2004, pp.45-60.
    • Harrison MD, Johnson PD, Wright PC. . In: Hollnagel, E, ed. Handbook of Cognitive Task Design. Mahwah, N.J.; London: Lawrence Erlbaum Associates, 2003, pp.503-524.

  • Conference Proceedings (inc. Abstracts)

    • Harrison MD, Masci P. . In: Sense, Feel, Design: INTERACT 2021. 2022, Porto: Springer, Cham.
    • Mentler T, Palanque P, Harrison MD, VanLaerhoven K, Masci P. . In: IFIP Conference on Human-Computer Interaction; INTERACT 2021 IFIP TC 13 Workshops. 2021, Bari: Springer International Publishing.
    • Campos JC, Harrison MD. . In: 2nd Workshop on Charting the Way towards Methods and Tools for Advanced Interactive Systems. 2019, Valencia, Spain: CEUR-WS.
    • Harrison MD, Masci P, Campos JC. . In: Software Technologies: Applications and Foundations. STAF 2018. 2018, Toulouse, France: Springer.
    • Harrison MD, Drinnan M, Campos JC, Masci P, Freitas L, di Maria C, Whitaker M. . In: Formal Aspects of Component Software (FACS 2017). 2017, Braga, Portugal: Springer.
    • Harrison MD, Campos JC, Rimvydas R, Curzon P. . In: 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems. 2016, Brussels, Belgium: ACM Press.
    • Harrison MD, Campos JC, Masci P, Curzon P. . In: 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". 2015, EAI.
    • Campos JC, Abade T, Silva JL, Harrison MD. . In: IWAAL 2015: Ambient Assisted Living. ICT-based Solutions in Real Life. 2015, Puerto Varas, Chile: Springer.
    • Sousa M, Campos JC, Alves M, Harrison MD. . In: AAAI Spring Symposium - Technical Report. 2014, Standford, CA, USA: AAAI Press.
    • Masci P, Ayoud A, Curzon P, Harrison MD, Lee I, Thimbleby H. . In: Proceedings of the 5th ACM SIGCHI symposium on Engineering interactive computing systems. 2013, London, UK: ACM Press.
    • Ruksenas R, Curzon P, Harrison MD. . In: IFM 2013: Proceedings of the 10th International Conference on Integrated Formal Methods. 2013, Turku, Finland: Springer.
    • Harrison MD, Masci P, Campos JC, Curzon P. . In: 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013). 2013, London, UK: Universitatsbibliothek TU Berlin.
    • Masci P, Huang H, Curzon P, Harrison MD. . In: NASA Formal Methods: 4th International Symposium (NFM). 2012, Norfolk, Virginia, USA: Springer.
    • Masci P, Furniss D, Curzon P, Harrison MD, Blandford A. . In: Software Engineering for Resilient Systems: Fourth International Workshop (SERENE). 2012, Pisa, Italy: Springer Verlag.
    • Thomas N, Harrison M, Zhao Y, Chen X. . In: Computer Performance Engineering: EPEW/UKPEW 2012. 2012, Edinburgh, UK: Springer.
    • Silva JL, Campos JC, Harrison MD. . In: Symposium on Engineering Interactive Computing Systems (EICS'12). 2012, Copenhagen, Denmark: ACM Press.
    • Chen X, Thomas N, Harrison M. . In: International Conference on Cyber-Enabled Distributed Computing and Knowledge Discovery, CyberC. 2011, Beijing, China: IEEE.
    • Campos JC, Harrison MD. . In: Fourth International Workshop on Formal Methods for Interactive Systems 2011. 2011, European Association of Software Science and Technology (E A S S T).
    • Massink M, Harrison MD, Latella D. . In: 25th annual ACM Symposium on Applied Computing. 2010, Sierre, Switzerland: ACM.
    • Dittmar A, Harrison MD. . In: Proceedings of the 2nd ACM SIGCHI symposium on Engineering Interactive Computing Systems. 2010, Berlin, Germany: ACM Press.
    • Silva JL, Ribeiro OR, Fernandes JM, Campos JC, Harrison MD. . In: 4a. Conferência Nacional em Interacção Humano-Computador (Interacção 2010). 2010, GPCG (Portuguese chapter of Eurographics).
    • Harrison MD, Massink M. . In: Electronic Notes in Theoretical Computer Science: 4th International Workshop on the Practical Application of Stochastic Modelling (PASM). 2010, Imperial College, London: Elsevier.
    • Massink M, Bracciali A, Latella D, Harrison M. . In: Proceedings of the 8th IEEE International Conference on Software Engineering And Formal Methods (SEFM2010). 2010, Pisa, Italy: IEEE.
    • Campos JC, Harrison MD. . In: EICS'09. Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems. 2009, Pittsburgh, PA, USA: ACM.
    • Harrison MD, Massink M, Latella D. . In: ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS). 2009, Pittsburgh, Pennsylvania, USA: ACM.
    • Harrison MD. . In: EICS'09: Proceedings of the 1st ACM SIGCHI symposium on Engineering interactive computing systems. 2009, Pittsburgh, PA, USA: Association for Computing Machinery.
    • Silva JL, Campos JC, Harrison MD. . In: EICS'09. Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems. 2009, Pittsburgh, Pennsylvania, USA: ACM.
    • Campos JC, Harrison MD. . In: Interactive Systems: Design, Specification and Verification. 15th International Workshop (DS-VIS). 2008, Kingston, Canada: Springer.
    • Doherty G, Campos J, Harrison MD. . In: Interactive Systems: Design, Specification and Verification. 15th International Workshop (DS-VIS). 2008, Kingston, Canada: Springer.
    • Harrison MD, Sujan M-A. . In: Computer Safety, Reliability, and Security: 27th International Conference (SAFECOMP). 2008, Â鶹´«Ã½ upon Tyne, UK: Springer.
    • Harrison MD, Kray C, Sun Z, Zhang H. . In: Engineering Interactive Systems: EIS 2007 Joint Working Conferences. 2008, Salamanca, Spain: Springer.
    • Harrison MD, Kray C, Campos JC. . In: Electronic Notes in Theoretical Computer Science: 2nd International Workshop on Formal Methods for Interactive Systems (FMIS). 2008, Lancaster, UK: Elsevier B.V.
    • Campos JC, Harrison MD. . In: Engineering Interactive Systems 2008: Second Conference on Human-Centered Software Engineering (HCSE). 2008, Salamanca, Spain: Springer.
    • Massink M, Latella D, ter Beek MH, Harrison MD, Loreti M. . In: Engineering Interactive Systems: Second Conference on Human-Centered Software Engineering, HCSE 2008 and 7th International Workshop on Task Models and Diagrams (TAMODIA). 2008, Pisa, Italy: Springer.
    • Thimbleby H, Harrison M. . In: People and Computers XXI. HCI...but not as we know it. 2007, University of Lancaster, UK: British Computer Society.
    • Harrison M, Kray C, Campos JC. . In: The Pre-proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS). 2007, Lancaster, UK: Queen Mary, University of London, Department of Computer Science.
    • Sujan MA, Harrison MD. . In: Safety and Reliability for Managing Risk. Proceedings of the 15th European Safety and Reliability Conference (ESREL). 2006, Estoril, Portugal: Taylor & Francis Group.
    • Sujan MA, Harrison MD, Steven A, Pearson PH, Vernon SJ. . In: 25th International Conference on Computer Safety, Reliability and Security (SAFECOMP). 2006, Gdansk, Poland: Springer.
    • Harrison MD, Kray C. . In: Workshop on Software Engineering Challenges for Ubiquitous Computing. 2006, Lancaster, UK: Lancaster University.
    • Gilroy SW, Harrison MD. . In: Engineering Human Computer Interaction and Interactive Systems. Joint Working Conferences EHCI-DSVIS 2004. 2005, Hamburg, Germany: Springer.
    • Loer K, Harrison MD. . In: Human-Computer-Interaction (INTERACT): IFIP TC13 International Conference. 2005, Rome, Italy: Springer.
    • Hildebrandt M, Loer KF, Harrison MD. . In: International Conference on Systems, Man and Cybernetics. 2004, The Hague, the Netherlands: IEEE.
    • Hildebrandt M, Harrison MD. . In: Human Factors and Ergonomics Society 48th Annual Meeting. 2004, New Orleans, Louisiana, USA: Human Factors and Ergonomics Society.
    • Smith SP, Harrison MD, Schupp BA. . In: Computer Safety, Reliability and Security (SAFECOMP). 2004, Potsdam, Germany: Springer.
    • Smith SP, Harrison MD. . In: Computer Safety, Reliability and Security: 22nd International Conference (SAFECOMP). 2003, Edinburgh, UK: Springer.
    • Hildebrandt M, Harrison MD. . In: Human Factors and Ergonomics Society: 47th Annual Meeting. 2003, Denver, Colorado, USA: Human Factors and Ergonomics Society.
    • Loer K, Harrison M. . In: 17th IEEE International Conference on Automated Systems Engineering (ASE). 2002, Edinburgh, UK: IEEE Computer Society Press.
    • Hildebrandt M, Harrison M. . In: 11th European Conference on Cognitive Ergonomics (ECCE). 2002, Catania, Sicily: European Association of Cognitive Ergonomics.
    • Smith SP, Harrison MD. . In: Software Reuse: Methods, Techniques, and Tools (ICSR-7). 2002, Austin, Texas, USA: Springer.
    • Loer K, Harrison MD. . In: 4th Werkstatt Mensch-Maschine-Systeme (ZMMS Spektrum Band 13). 2002, Berlin, Germany: VDI Verlag, Fortschritt-Berichte VDI.
    • Smith SP, Harrison MD. . In: 9th International Workshop on Interactive Systems: Design, Specification and Verification (DSV-IS). 2002, Rostock, Germany: Springer-Verlag.
    • Harrison MD, Johnson PD, Wright PC. . In: Components of System Safety: Proceedings of the Tenth Safety-critical Systems Symposium. 2002, Southampton, UK: Springer.
    • Smith SP, Harrison MD. . In: ACM Symposium on Applied Computing (SAC). 2002, Madrid, Spain: ACM.
    • Pocock S, Harrison MD, Wright PC, Johnson P. . In: Human Computer Interaction - INTERACT'01, IFIP TC.13 International Conference. 2001, Tokyo, Japan: IOS Press.
    • Willans JC, Harrison M. . In: Engineering for Human-Computer Interaction. 8th IFIP International Conference (EHCI). 2001, Toronto, Canada: Springer.
    • Loer K, Harrison M. . In: Interactive Systems. Design, Specification and Verification. 7th International Workshop, DSV-IS. 2001, Limerick, Ireland: Springer-Verlag.
    • Johnson P, Harrison MD, Wright P. . In: Human Interfaces in Control Rooms, Cockpits and Command Centres: 2nd International Conference on People in Control. 2001, Manchester, UK: IEE Press.
    • Griffiths AD, Harrison MD, Dearden AM. . In: Human-Computer Interaction (INTERACT). 1999, Edinburgh, UK: IOS Press.
    • Campos JC, Harrison MD. . In: Proceedings of the Eurographics Workshop on Design, Specification and Verification of Interactive Systems. 1998, Abingdon, UK: Springer.
    • Doherty G, Campos JC, Harrison MD. . In: Proceedings of the Formal Aspects of the Human Computer Interaction, BCS-FACS Workshop. 1998, SHU Press.
    • Doherty G, Harrison MD. . In: Proceedings of the Eurographics Workshop on Design, Specification and Verification of Interactive Systems. 1998, Abingdon, UK: Springer.
    • Dearden AM, Harrison MD. . In: 16th International Conference on Computer Safety, Reliability and Security (SAFECOMP). 1997, York, UK: Springer.
    • Fields B, Wright P, Harrison M. . In: Human-Computer Interaction: IFIP TC13 International Conference on Human-Computer Interaction (INTERACT). 1997, Sydney, Australia: Chapman and Hall.
    • McCarthy JC, Wright PC, Healey P, Dearden A, Harrison MD. . In: Proceedings of the International ACM SIGGROUP Conference on Supporting Group Work: The Integration Challenge (GROUP). 1997, Pheonix, Arizona, USA: ACM.
    • Campos JC, Harrison MD. . In: Design, Specification, and Verification of Interactive Systems’97. Proceedings of the Eurographics Workshop. 1997, Grenada, Spain: Springer.
    • Doherty G, Harrison MD. . In: Design, Specification, and Verification of Interactive Systems’97. Proceedings of the Eurographics Workshop. 1997, Grenada, Spain: Springer.
    • Harrison M, Fields R, Wright PC. . In: BCS-FACS Workshop on Formal Aspects of the Human Computer Interface. 1996, Sheffield Hallam University, UK: Springer in collaboration with the British Computer Society.
    • Dearden AM, Harrison MD. . In: Design Specification and Verification of Interactive Systems '96: Proceedings of the Eurographics Workshop. 1996, Namur, Belgium: Springer.
    • Dearden AM, Harrison MD. . In: Safety-Critical Systems: the Convergence of High Tech and Human Factors. Proceedings of the Fourth Safety-critical Systems Symposium. 1996, Leeds, UK: Springer.
    • Wright PC, Fields B, Harrison MD. . In: Cognition and the worksystem. Proceedings of the 8th European conference on cognitive ergonomics. 1996, Grenada, Spain: European Association of Cognitive Ergonomics.

  • Edited Books

    • Harrison MD, Sujan M-A, ed. . Berlin, Germany: Springer-Verlag, 2008.
    • Gilroy SW, Harrison MD, ed. . Berlin; New York: Springer, 2006.

  • Editorial

    • Harrison MD. . Software Engineering Journal 1996, 11(6), 322.

  • Reports

    • Harrison MD, Campos JC, Masci P. Patterns and templates for automated verification of user interface software design in PVS. Â鶹´«Ã½, 2015. School of Computing Science Technical Report Series 1485. Submitted.
    • Massink M, Latella D, Bracciali A, Harrison M. . Pisa, Italy: CNR-ISTI, 2010. Technical Report TR012.
    • Campos JC, Doherty G, Harrison MD. . Braga, ortugal: University of Minho, 2009. Technical Report DI-CCTC-09-17.
    • Harrison MD, Loer K. . Â鶹´«Ã½ upon Tyne: School of Computing Science, University of Â鶹´«Ã½ upon Tyne, 2006. School of Computing Science Technical Report Series 980.
    • Loer K, Harrison MD. . Â鶹´«Ã½ upon Tyne: School of Computing Science, University of Â鶹´«Ã½ upon Tyne, 2004. School of Computing Science Technical Report Series 876.
    • Loer K, Harrison MD. . Â鶹´«Ã½ upon Tyne: School of Computing Science, University of Â鶹´«Ã½ upon Tyne, 2004. School of Computing Science Technical Report Series 873.
    • Hildebrandt M, Harrison M. . Glasgow, UK: Department of Computing Science, University of Glasgow, 2002. GIST Technical Report Series G2002-1.
    • Pocock S, Fields R, Harrison M, Wright P. . York, UK: Department of Computer Science, University of York, 2001. 336.