• DocumentCode
    2130480
  • Title

    Safety-assured development of the GPCA infusion pump software

  • Author

    Kim, BaekGyu ; Ayoub, Anaheed ; Sokolsky, Oleg ; Lee, Insup ; Jones, Paul ; Zhang, Yi ; Jetley, Raoul

  • Author_Institution
    Comput. & Inf. Sci. Dept., Univ. of Pennsylvania, Philadelphia, PA, USA
  • fYear
    2011
  • fDate
    9-14 Oct. 2011
  • Firstpage
    155
  • Lastpage
    164
  • 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.
  • Keywords
    automata theory; medical computing; program verification; GPCA infusion pump software; PCA pump; TIMES tool; UPPAAL tool; US Food and Drug Administration; conformance testing; generic PCA reference model; model-driven engineering; patient-controlled analgesic; safety-assured development; timed automata; Automata; Drugs; Principal component analysis; Reservoirs; Safety; Software; Testing; PCA infusion pump; code synthesis; formalization; model-based engineering; timed automata; verification;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Embedded Software (EMSOFT), 2011 Proceedings of the International Conference on
  • Conference_Location
    Taipei
  • Print_ISBN
    978-1-4503-0714-7
  • Type

    conf

  • Filename
    6064522