Skip to main content
Article
Safety-Assured Development of the GPCA Infusion Pump Software
International Conference on Embedded Software (EMSOFT 2011)
  • BaekGyu Kim, University of Pennsylvania
  • Anaheed Ayoub, University of Pennsylvania
  • Oleg Sokolsky, University of Pennsylvania
  • Insup Lee, University of Pennsylvania
  • Paul Jones, U.S. Food and Drug Administration
  • Yi Zhang, U.S. Food and Drug Administration
  • Raoul Jetley, U.S. Food and Drug Administration
Date of this Version
10-1-2011
Document Type
Conference Paper
Comments
The International Conference on Embedded Software (EMSOFT 2011), Taipei, Taiwan, October 9-14 2011.
Abstract

This paper presents our effort of using model-driven engineering to establish a safety-assured implementation of Patient-Controlled Analgesic (PCA) infusion pump software based on the generic PCA reference model provided by the U.S. Food and Drug Administration (FDA). The reference model was first translated into a network of timed automata using the UPPAAL tool. Its safety properties were then assured according to the set of generic safety requirements also provided by the FDA. Once the safety of the reference model was established, we applied the TIMES tool to automatically generate platform-independent code as its preliminary implementation. The code was then equipped with auxiliary facilities to interface with pump hardware and deployed onto a real PCA pump. Experiments show that the code worked correctly and effectively with the real pump. To assure that the code does not introduce any violation of the safety requirements, we also developed a testbed to check the consistency between the reference model and the code through conformance testing. Challenges encountered and lessons learned during our work are also discussed in this paper.

DOI
10.1145/2038642.2038667
Copyright/Permission Statement
© ACM 2011. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the International Conference on Embedded Software (EMSOFT 2011), http://dx.doi.org/10.1145/2038642.2038667.
Keywords
  • Software,
  • Program Verification,
  • Formal methods,
  • Model checking,
  • Validation,
  • PCA infusion pump,
  • model-based engineering,
  • formalization,
  • verification,
  • code synthesis,
  • timed automata
Citation Information
BaekGyu Kim, Anaheed Ayoub, Oleg Sokolsky, Insup Lee, et al.. "Safety-Assured Development of the GPCA Infusion Pump Software" International Conference on Embedded Software (EMSOFT 2011) (2011) p. 155 - 164
Available at: http://works.bepress.com/yi_zhang/2/