Overview

The Generic Infusion Pump (GIP) project is aiming at developing a set of generic infusion pump models and reference specifications that can be used as a reference standard to verify safety properties in different classes of infusion pumps. As a first step, our collaborator, Food and Drug Administration (FDA), released the Generic Patient Controlled Analgesic (GPCA) infusion pump model along with hazard analysis and safety requirements.

We focus on applying the safety-assured model-based software development process toward the GPCA pump reference implementation. The model-based development process consists of the following phases : (1) Formal Modeling and Verification : the GPCA model and safety requirements are formalized that can be formally verified using model-checker (e.g., UPPAAL). (2) Code-Generation : the formally verified model is automatically synthesized into platform-independent code using a code-synthesis tool (e.g., TIMES). (3) Deployment : the generated platform-independent code is executed on top of a virtual layer that exhibits deterministic infusion operations across different target platforms.

Toward a certifiable implementation, we claim “our GPCA pump reference implementation is safe and effective” through safety cases. Two development phases – implementation and safety cases – cooperate each other to achieve this goal; the implementation cycle feeds evidences to the safety case, and fills safety gaps found from the safety case. From this joint activity, we expect that safety cases contribute not only to the certification process, but also to the development of safer implementation.

The contribution of this project is to create safety-assured and certifiable artifacts that compose PCA pump systems - such as formal model, source code, and safety cases. These artifacts are opened to both device manufacturers and research communities so that they play a role of exemplar of safety-assured model-based development in infusion pump domains as well as other safety-critical systems.

Video Clips

• Link to the page

Resources

• Model download
• Source code download
• How to run the program download

Publications

• (Poster) Safety-Assured Model-Based Implementation of the GPCA Infusion Pump Software
  Baek-Gyu Kim, Design, Automation and Test in Europe (DATE 2015) PhD Forum. Grenoble, France, Mar 2015
• Platform-Specific Timing Verification Framework in Model-Based Implementation
  BaekGyu Kim, Lu Feng, Linh T.X. Phan, Oleg Sokolsky and Insup Lee. Design, Automation and Test in Europe (DATE 2015). Grenoble, France, Mar 2015
• From Requirements to Code: Model Based Development of a Medical Cyber Physical System
  Anitha Murugesan, Michael Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, Mats Heimdahl, Baek-Gyu Kim, Oleg Sokolsky and Insup Lee. FHIES/SEHC 2014. Washington, D.C., USA, July 2014
• A Layered Approach for Timing Testing in the Model-Based Implementation
  BaekGyu Kim, Hyeon I Hwang, Taejoon Park, Sanghyuk Son, Insup Lee. Design, Automation and Test in Europe (DATE 2014). Dresden, Germany, Mar 2014
• A Causality Analysis Framework for Component-based Real-time Systems
  Shaohui Wang, Anaheed Ayoub, BaekGyu Kim, Gregor ossler, Oleg Sokolsky, and Insup Lee. Runtime Verification (RV2013), INRIA Rennes, France
• Platform-Dependent Code Generation for Embedded Real-Time Software
  BaekGyu Kim, Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. International Conference on Compilers, Architectures and Synthesis of Embedded Systems (CASES 2013). Montreal, Canada, October 2013
• (Demo) Platform Dependent Code Generation of Real-Time Embedded Software
  BaekGyu Kim, Insup Lee, Linh T.X. Phan, Oleg Sokolsky. ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2013), Philadelphia, USA
• A Model-Based I/O Interface Synthesis Framework for the Cross-Platform Software Modeling
  BaekGyu Kim, Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. IEEE International Symposium on Rapid System Prototyping (RSP 2012). Tampere, Finland, October 2012
• A Systematic Approach to Justifying Sufficient Confidence in Software Safety Arguments
  Anaheed Ayoub, BaekGyu Kim, Insup Lee, and Oleg Sokolsky. International Conference on Computer Safety, Reliability and Security (SAFECOMP 2012). Magdeburg, Germany, September 2012
• A Safety Case Pattern for Model-Based Development Approach
  Anaheed Ayoub, Baek-Gyu Kim, Insup Lee and Oleg Sokolsky. NASA Formal Methods Symposium (NFM 2012). Norfolk, VA, April 2012
• Challenges and Research Directions in Medical Cyber-Physical Systems
  Insup Lee, Oleg Sokolsky, Sanjian Chen, John Hatcliff, Eunkyoung Jee, BaekGyu Kim, Andrew King, Margaret Mullen-Fortino, Soojin Park, Alexander Roederer, and Krishna Venkatasubramanian. In Special Issue on Cyber-Physical Systems, Proceedings of the IEEE, Volume 100, Issue 1, pp.75-90, January 2012
• Safety-Assured Development of the GPCA Infusion Pump Software
  BaekGyu Kim, Anaheed Ayoub, Oleg Sokolsky, Insup Lee, Paul Jones, Yi Zhang, and Raoul Jetley. International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011

Acknowledgements

This research is support in part by NSF CPS large grant (NSF CNS-1035715) and NSF FDA Scholar-in-Residence grant (NSF CNS-1042829). We are grateful to Paul Jones and Yi Zhang at the FDA for advice and discussions.