Generic PCA Infusion Pump Reference Implementation

Description

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.

Current Members
Insup Lee profile photo
Insup Lee
Oleg Sokolsky's Profile Photo
Oleg Sokolsky
Publications
A Safety Case Pattern for Model-Based Development Approach
Anaheed Ayoub, Baek-Gyu Kim, Insup Lee and Oleg Sokolsky.

Accepted in 4th NASA FORMAL METHODS SYMPOSIUM (NFM2012), Virginia, USA, April 9-14 2012.