A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices

  • Paolo MasciEmail author
  • Yi Zhang
  • Paul Jones
  • José C. Campos
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10469)


Formal methods technologies have the potential to verify the usability and safety of user interface (UI) software design in medical devices, enabling significant reductions in use errors and consequential safety incidents with such devices. This however depends on comprehensive and verifiable safety requirements to leverage these techniques for detecting and preventing flaws in UI software that can induce use errors. This paper presents a hazard analysis method that extends Leveson’s System Theoretic Process Analysis (STPA) with a comprehensive set of causal factor categories, so as to provide developers with clear guidelines for systematic identification of use-related hazards associated with medical devices, their causes embedded in UI software design, and safety requirements for mitigating such hazards. The method is evaluated with a case study on the Gantry-2 radiation therapy system, which demonstrates that (1) as compared to standard STPA, our method allowed us to identify more UI software design issues likely to cause use-related hazards; and (2) the identified UI software design issues facilitated the definition of precise, verifiable safety requirements for UI software, which could be readily formalized in verification tools such as Prototype Verification System (PVS).


Requirements identification/formalization User interface software Medical devices 



Sandy Weininger (FDA), Scott Thiel (Navigant Consulting, Inc.), Michelle Jump (Stryker), Stefania Gnesi (ISTI/CNR) and the CHI+MED team ( provided useful feedback and inputs. Paolo Masci’s work is supported by the North Portugal Regional Operational Programme (NORTE 2020) under the PORTUGAL 2020 Partnership Agreement, and by the European Regional Development Fund (ERDF) within Project “NORTE-01-0145-FEDER-000016”.


  1. 1.
    Association for the Advancement of Medical Instrumentation: Infusing patients safely: Priority issues from the AAMI/FDA Infusion Device Summit. AAMI (2010)Google Scholar
  2. 2.
    Blandine, A.: System Theoretic Hazard Analysis applied to the risk review of complex systems. Ph.D. thesis, MIT (2012)Google Scholar
  3. 3.
    Bolton, M.L., Bass, E.J.: A method for the formal verification of human-interactive systems. In: Proceedings of the Human Factors and Ergonomics Society Annual Meeting, vol. 53(12), pp. 764–768. Sage Publications (2009). doi: 10.1177/154193120905301201CrossRefGoogle Scholar
  4. 4.
    Bowen, J., Reeves, S.: A simplified Z semantics for presentation interaction models. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 148–162. Springer, Cham (2014). doi: 10.1007/978-3-319-06410-9_11CrossRefGoogle Scholar
  5. 5.
    Ericson, C.: Hazard Analysis Techniques for System Safety. Wiley, New York (2015). doi: 10.1002/0471739421.ch1CrossRefGoogle Scholar
  6. 6.
    Campos, J.C., Harrison, M.D.: Interaction engineering using the IVY tool. In: EICS 2009, pp. 35–44. ACM (2009). doi: 10.1145/1570433.1570442
  7. 7.
    Chudleigh, M., Clare, J.N.: The benefits of SUSI: Safety analysis of user system interaction. In: Górski, J. (ed.) SAFECOMP 1993, pp. 123–132. Springer, London (1993). doi: 10.1007/978-1-4471-2061-2_13CrossRefGoogle Scholar
  8. 8.
    Dokas, I., Feehan, J., Imran, S.: EWaSAP: an early warning sign identification approach based on a systemic hazard analysis. Saf. Sci. 58, 11–26 (2013). doi: 10.1016/j.ssci.2013.03.013CrossRefGoogle Scholar
  9. 9.
    Food and Drug Administration (FDA): Class 2 Device Recall ACCUCHEK Connect Diabetes Management App (2015).
  10. 10.
    Harrison, M.D., Campos, J.C., Masci, P.: Reusing models and properties in the analysis of similar interactive devices. Innov. Syst. Softw. Eng. 11(2), 95–111 (2015). doi: 10.1007/s11334-013-0201-3CrossRefGoogle Scholar
  11. 11.
    Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Demonstrating that medical devices satisfy user related safety requirements. In: Huhn, M., Williams, L. (eds.) Software Engineering in Health Care: 4th International Symposium, FHIES 2014, and 6th International Workshop, SEHC 2014, Washington, DC, USA, July 17–18, 2014, Revised Selected Papers, pp. 113–128. Springer International Publishing, Cham (2017). doi: 10.1007/978-3-319-63194-3_8. ISBN: 978-3-319-63194-3CrossRefGoogle Scholar
  12. 12.
    Hussey, A.: HAZOP analysis of formal models of safety-critical interactive systems. In: Koornneef, F., Meulen, M. (eds.) SAFECOMP 2000. LNCS, vol. 1943, pp. 371–381. Springer, Heidelberg (2000). doi: 10.1007/3-540-40891-6_32CrossRefGoogle Scholar
  13. 13.
    Ishikawa, K., Lu, D.J.: What is Total Quality Control? The Japanese Way. Prentice Hall Business Classics, Prentice-Hall, Englewood Cliffs (1985)Google Scholar
  14. 14.
    Kletz, T.A.: Hazop and hazan: identifying and assessing process industry hazards. Disaster Prev. Manage. Int. J. 10(1), 30–31 (2001). doi: 10.1108/dpm.2001. Scholar
  15. 15.
    Leape, L.L., Berwick, D.M.: Five years after to err is human: what have we learned? JAMA 293(19) (2005). doi: 10.1001/jama.293.19.2384CrossRefGoogle Scholar
  16. 16.
    Lee, W.S., Grosh, D.L., Tillman, F.A., Lie, C.H.: Fault tree analysis, methods, and applications: a review. IEEE Trans. Reliab. 34(3), 194–203 (1985). doi: 10.1109/TR.1985.5222114CrossRefzbMATHGoogle Scholar
  17. 17.
    Leveson, N.: Engineering a Safer World. MIT Press, Cambridge (2011)Google Scholar
  18. 18.
    Leveson, N.: A systems approach to risk management through leading safety indicators. Reliab. Eng. Syst. Saf. 136, 17–34 (2015). doi: 10.1016/j.ress.2014.10.008CrossRefGoogle Scholar
  19. 19.
    Masci, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H.: Formal verification of medical device user interfaces using PVS. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 200–214. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54804-8_14CrossRefGoogle Scholar
  20. 20.
    Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA Regulation as an example. In: EICS 2013, pp. 81–90. ACM (2013). doi: 10.1145/2494603.2480302
  21. 21.
    Masci, P., Curzon, P., Furniss, D., Blandford, A.: Using PVS to support the analysis of distributed cognition systems. Innov. Syst. Softw. Eng. 11(2), 113–130 (2015). doi: 10.1007/s11334-013-0202-2CrossRefGoogle Scholar
  22. 22.
    Masci, P., Furniss, D., Curzon, P., Harrison, M.D., Blandford, A.: Supporting field investigators with PVS: a case study in the healthcare domain. In: Avgeriou, P. (ed.) SERENE 2012. LNCS, vol. 7527, pp. 150–164. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-33176-3_11CrossRefGoogle Scholar
  23. 23.
    Nielsen, J.: Usability Engineering. Morgan Kaufmann, San Francisco (1993). doi: 10.1016/B978-0-08-052029-2.50001-2CrossRefzbMATHGoogle Scholar
  24. 24.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). doi: 10.1007/3-540-55602-8_217CrossRefGoogle Scholar
  25. 25.
    Masci, P., Rukšėnas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.: The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. Innov. Syst. Softw. Eng. 11(2), 73–93 (2015). doi: 10.1007/s11334-013-0200-4CrossRefGoogle Scholar
  26. 26.
    Paterno, F., Mancini, C., Meniconi, S.: ConcurTaskTrees: a diagrammatic notation for specifying task models. In: Howard, S., Hammond, J., Lindgaard, G. (eds.) Human-Computer Interaction INTERACT ’97. ITIFIP, pp. 362–369. Springer, Boston, MA (1997). doi: 10.1007/978-0-387-35175-9_58CrossRefGoogle Scholar
  27. 27.
    Procter, S., Hatcliff, J.: An architecturally-integrated, systems-based hazard analysis for medical applications. In: MEMOCODE 2014, pp. 124–133. IEEE (2014). doi: 10.1109/MEMCOD.2014.6961850
  28. 28.
    Rukšėnas, R., Curzon, P., Back, J., Blandford, A.: Formal modelling of cognitive interpretation. In: Doherty, G., Blandford, A. (eds.) DSV-IS 2006. LNCS, vol. 4323, pp. 123–136. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-69554-7_10CrossRefGoogle Scholar
  29. 29.
    Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. Reliab. Eng. Syst. Saf. 75(2), 167–177 (2002). doi: 10.1016/S0951-8320(01)00092-8CrossRefGoogle Scholar
  30. 30.
    Stamatis, D.: Failure Mode And Effect Analysis. ASQ Quality Press, Milwaukee (2003)Google Scholar
  31. 31.
    Thornberry, C.: Extending the human-controller methodology in systems-theoretic process analysis (STPA). Ph.D. thesis, MIT (2014)Google Scholar

Copyright information

© Springer International Publishing AG (outside the US) 2017

Authors and Affiliations

  • Paolo Masci
    • 1
    Email author
  • Yi Zhang
    • 2
  • Paul Jones
    • 2
  • José C. Campos
    • 1
  1. 1.INESC TECUniversidade Do MinhoBragaPortugal
  2. 2.US Food and Drug AdministrationSilver SpringUSA

Personalised recommendations