Skip to main content

2017 | OriginalPaper | Buchkapitel

Demonstrating that Medical Devices Satisfy User Related Safety Requirements

verfasst von : Michael D. Harrison, Paolo Masci, Jose Creissac Campos, Paul Curzon

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

One way of contributing to a demonstration that a medical device is acceptably safe is to show that the device satisfies a set of requirements known to mitigate hazards. This paper describes experience using formal techniques to model an IV infusion device and to prove that the modelled device captures a set of requirements. The requirements chosen for the study are based on a draft proposal developed by the US Food and Drug Administration (FDA). A major contributor to device related errors are (user) interaction errors. For this reason the chosen models and requirements focus on user interface related issues.

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!

Fußnoten
1
The models can be found at http://​hcispecs.​di.​uminho.​pt.
 
Literatur
1.
Zurück zum Zitat Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
2.
Zurück zum Zitat Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O., Ray, A., Zhang, Y.: Generic infusion pump hazard analysis and safety requirements. Technical report MS-CIS-08-31, University of Pennsylvania, February 2009 Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O., Ray, A., Zhang, Y.: Generic infusion pump hazard analysis and safety requirements. Technical report MS-CIS-08-31, University of Pennsylvania, February 2009
3.
Zurück zum Zitat Campos, J.C., Harrison, M.D.: Interaction engineering using the IVY tool. In: Calvary, G., Graham, T.C.N., Gray, P. (eds.) Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pp. 35–44. ACM Press (2009) Campos, J.C., Harrison, M.D.: Interaction engineering using the IVY tool. In: Calvary, G., Graham, T.C.N., Gray, P. (eds.) Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pp. 35–44. ACM Press (2009)
4.
Zurück zum Zitat Cardinal Health Inc.: Alaris GP volumetric pump: directions for use. Technical report, Cardinal Health, 1180 Rolle, Switzerland (2006) Cardinal Health Inc.: Alaris GP volumetric pump: directions for use. Technical report, Cardinal Health, 1180 Rolle, Switzerland (2006)
5.
Zurück zum Zitat Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_29 CrossRef Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45657-0_​29 CrossRef
6.
Zurück zum Zitat Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999) Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
7.
Zurück zum Zitat Gelman, G.E., Feigh, K.M., Rushby, J.: Example of a complementary use of model checking and agent-based simulation. In: 2013 IEEE International Conference on Systems, Man, and Cybernetics (SMC), pp. 900–905, October 2013 Gelman, G.E., Feigh, K.M., Rushby, J.: Example of a complementary use of model checking and agent-based simulation. In: 2013 IEEE International Conference on Systems, Man, and Cybernetics (SMC), pp. 900–905, October 2013
8.
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, April 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, April 2013
9.
Zurück zum Zitat Heitmeyer, J.C., Kirby Jr., J., Labaw, B.: Applying the SRC requirements method to a weapons control panel: an experience report. In: Proceedings of the Second Workshop on Formal Methods in Software Practice (FMSP 1998), pp. 92–102 (1998) Heitmeyer, J.C., Kirby Jr., J., Labaw, B.: Applying the SRC requirements method to a weapons control panel: an experience report. In: Proceedings of the Second Workshop on Formal Methods in Software Practice (FMSP 1998), pp. 92–102 (1998)
11.
Zurück zum Zitat Jetley, R., Purushothaman Iyer, S., Jones, P.L.: A formal methods approach to medical device review. Computer 39(4), 61–67 (2006)CrossRef Jetley, R., Purushothaman Iyer, S., Jones, P.L.: A formal methods approach to medical device review. Computer 39(4), 61–67 (2006)CrossRef
12.
Zurück zum Zitat Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety (Engineering Systems). MIT Press, Cambridge (2011) Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety (Engineering Systems). MIT Press, Cambridge (2011)
13.
Zurück zum Zitat Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Sokolsky, O., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: Proceedings ACM Symposium Engineering Interactive Systems (EICS 2013), pp. 81–90. ACM Press (2013) Masci, P., Ayoub, A., Curzon, P., Harrison, M.D., Lee, I., Sokolsky, O., Thimbleby, H.: Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: Proceedings ACM Symposium Engineering Interactive Systems (EICS 2013), pp. 81–90. ACM Press (2013)
14.
Zurück zum Zitat Masci, P., Ayoub, A., Curzon, P., Lee, I., Sokolsky, O., Thimbleby, H.: Model-based development of the generic PCA infusion pump user interface prototype in PVS. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 228–240. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40793-2_21 CrossRef Masci, P., Ayoub, A., Curzon, P., Lee, I., Sokolsky, O., Thimbleby, H.: Model-based development of the generic PCA infusion pump user interface prototype in PVS. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 228–240. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40793-2_​21 CrossRef
15.
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
16.
Zurück zum Zitat Masci, P., Zhang, Y., Jones, P., Thimbleby, H., Curzon, P.: A generic user interface architecture for analyzing use hazards in infusion pump software. In: Turau, V., Kwiatkowska, M., Mangharam, R., Weyer, C. (eds.) 5th Workshop on Medical Cyber-Physical Systems. OpenAccess Series in Informatics (OASIcs), vol. 36, pp. 1–14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2014) Masci, P., Zhang, Y., Jones, P., Thimbleby, H., Curzon, P.: A generic user interface architecture for analyzing use hazards in infusion pump software. In: Turau, V., Kwiatkowska, M., Mangharam, R., Weyer, C. (eds.) 5th Workshop on Medical Cyber-Physical Systems. OpenAccess Series in Informatics (OASIcs), vol. 36, pp. 1–14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2014)
17.
Zurück zum Zitat Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.E.: Compositional verification of a medical device system. In: Proceedings ACM High Integrity Language Technologies (HILT 2013). ACM Press (2013) Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.E.: Compositional verification of a medical device system. In: Proceedings ACM High Integrity Language Technologies (HILT 2013). ACM Press (2013)
18.
Zurück zum Zitat 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_217 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_​217
Metadaten
Titel
Demonstrating that Medical Devices Satisfy User Related Safety Requirements
verfasst von
Michael D. Harrison
Paolo Masci
Jose Creissac Campos
Paul Curzon
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-63194-3_8