Skip to main content

2017 | OriginalPaper | Buchkapitel

Using PVSio-web to Demonstrate Software Issues in Medical User Interfaces

verfasst von : Paolo Masci, Patrick Oladimeji, Paul Curzon, Harold Thimbleby

Erschienen in: Software Engineering in Health Care

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We have used formal methods technology to investigate software and user interface design issues that may induce use error in medical devices. Our approach is based on mathematical models that capture safety concerns related to the use of a device. We analysed nine commercial medical devices from six manufacturers with our approach, and precisely identified 30 design issues. All identified issues can induce use errors that could lead to adverse clinical consequences, such as numbers being incorrectly entered. An issue with formal approaches is in making results accessible to developers, human factors experts and clinicians. In this paper, we use our tool PVSio-web to demonstrate the identified issues: PVSio-web allows us to generate realistic and interactive user interface prototypes from the same mathematical models used for analysis. Users can explore the behaviour of the prototypes by pressing buttons on realistic user interfaces that reproduce the functionality and visual representation of the real devices. Users can examine the device behaviour resulting from any interaction. Key sequences identified from analysis can be used to explore in detail the identified design issues in an accessible way.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat Cauchi, A., Gimblett, A., Thimbleby, H.W., Curzon, P., Masci, P.: Safer 5-key number entry user interfaces using differential formal analysis. In: 26th Annual BCS Interaction Specialist Group Conference on People and Computers (BCS-HCI), pp. 29–38. British Computer Society (2012) Cauchi, A., Gimblett, A., Thimbleby, H.W., Curzon, P., Masci, P.: Safer 5-key number entry user interfaces using differential formal analysis. In: 26th Annual BCS Interaction Specialist Group Conference on People and Computers (BCS-HCI), pp. 29–38. British Computer Society (2012)
2.
Zurück zum Zitat Center for Devices and Radiological Health: US Food and Drug Administration. Infusion Pump Improvement Initiative, White Paper (2010) Center for Devices and Radiological Health: US Food and Drug Administration. Infusion Pump Improvement Initiative, White Paper (2010)
3.
Zurück zum Zitat Harrison, M.D., Campos, J.C., Masci, P.: Reusing models and properties in the analysis of similar interactive devices. In: Innovations in Systems and Software Engineering, pp. 1–17 (2013) Harrison, M.D., Campos, J.C., Masci, P.: Reusing models and properties in the analysis of similar interactive devices. In: Innovations in Systems and Software Engineering, pp. 1–17 (2013)
4.
Zurück zum Zitat Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Demonstrating that medical devices satisfy user related safety requirements. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (2014) Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Demonstrating that medical devices satisfy user related safety requirements. In: 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (2014)
5.
Zurück zum Zitat Institute for Safe Medication Practices (ISMP). List of error-prone abbreviations, symbols and dose designations (2006) Institute for Safe Medication Practices (ISMP). List of error-prone abbreviations, symbols and dose designations (2006)
6.
Zurück zum Zitat Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Thimbleby, H.W.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2013). ACM Digital Library (2013) Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Thimbleby, H.W.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2013). ACM Digital Library (2013)
7.
Zurück zum Zitat Masci, P., Rukšėnas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.W.: On formalising interactive number entry on infusion pumps. ECEASST 45 (2011) Masci, P., Rukšėnas, R., Oladimeji, P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.W.: On formalising interactive number entry on infusion pumps. ECEASST 45 (2011)
8.
Zurück zum Zitat Masci, P., Rukšėnas, R., Oladimeji P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.W.: The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. In: Innovations in Systems and Software Engineering, pp. 1–21 (2013) Masci, P., Rukšėnas, R., Oladimeji P., Cauchi, A., Gimblett, A., Li, Y., Curzon, P., Thimbleby, H.W.: The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. In: Innovations in Systems and Software Engineering, pp. 1–21 (2013)
9.
Zurück zum Zitat 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_14 CrossRef 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_​14 CrossRef
11.
Zurück zum Zitat Munoz, C.: Rapid prototyping in PVS. National Institute of Aerospace, Hampton, VA, USA, Technical report NIA, 3 (2003) Munoz, C.: Rapid prototyping in PVS. National Institute of Aerospace, Hampton, VA, USA, Technical report NIA, 3 (2003)
12.
Zurück zum Zitat Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.W.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. In: 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013) (2013). http://pvsioweb.org/ Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.W.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. In: 5th International Workshop on Formal Methods for Interactive Systems (FMIS 2013) (2013). http://​pvsioweb.​org/​
13.
Zurück zum Zitat Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996). doi:10.1007/3-540-61474-5_91 CrossRef Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996). doi:10.​1007/​3-540-61474-5_​91 CrossRef
14.
Zurück zum Zitat Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709–720 (1998)CrossRef Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709–720 (1998)CrossRef
15.
Metadaten
Titel
Using PVSio-web to Demonstrate Software Issues in Medical User Interfaces
verfasst von
Paolo Masci
Patrick Oladimeji
Paul Curzon
Harold Thimbleby
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-63194-3_14