RTG Home  |   PRECISE  |   CIS Home  |   Penn Engineering  |   Penn
Generic PCA Infusion Pump Reference Implementation


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


Current Members




National Science Foundation 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.

RTG Home  |   PRECISE  |   CIS Home  |   Penn Engineering  |   Penn