Generic Patient Controlled Analgesia Infusion Pump Project
Infusion pumps are used to accurately infuse liquids into a patient's bloodstream. Unfortunately, infusion pumps have been involved in many incidents that have resulted in harm to the patient. The US Food and Drug Administration (FDA), through its Infusion Pump Improvement Initiative has sought to pro-actively promote the safe use of these devices by establishing additional requirements for infusion pump manufacturers. In this context, the research community---in collaboration with the FDA---is exploring various methods to improve the safety of infusion pump systems.
Our aim is to contribute to this FDA initiative by providing an archetype of system development artifacts for a Generic Patient Controlled Analgesia Infusion Pump (GPCA) system; a collection of artifacts that could serve as a generic reference standard used by researchers, practitioners, and certification authorities while developing and reviewing assurance cases.
Requirements
To provide a well argued assurance case, it is absolutely crucial to have a suitable set of system requirements from which to start; to argue that a hazard is not present in a system we must first demonstrate the system requirements do not allow the hazard to occur. Absent such requirements, the assurance case cannot be made.
Click here to view the requirements documents for the GPCA system.
Models
Models have proved useful during requirements elicitation, analysis and validation and verification of complex safety related control systems. We developed architectural models to visualize and understand the system boundaries, control models in the continuous domain to help identify the missing requirements on the physical side of our cyber-physical system and State flow models to understand detailed software requirements and perform rigorous validation. For the modeling activity we choose Simulink - one of the most widely used modeling tools.
The following are the modeling artifacts for the GPCA system.
Latest Version 2.0Older Versions of the Models - Version 1.0
Verification
Decomposition into subsystems allows for intellectual control, as well as enabling different subsystems to be created by distinct teams. However, demonstrating that a complex system satisfies its requirements when the subsystems are composed is a challenging problem. For the GPCA, we represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe the requirements at different levels of abstraction for compositional verification. The component-level behavior for the model is described in Simulink/Stateflow. We assemble proofs of system level properties by using the Simulink Design Verifier to establish component-level properties and an open-source plug-in for the OSATE AADL environment to perform the compositional verification of the architecture. This combination of verification tools allows us to iteratively explore design and verification of detailed behavioral models, and to scale formal analysis to large software systems.
Click here to download the verification suite for the GPCA system.
Click here to watch the project overview video .
Source Code
Automatic code generation from the model is a useful byproduct of using the State flow tool's code generator. We generate C code using the Software State flow Model. This C code can be used to test the software on real hardware pumps.
Click here to download the C code generated from the most recent Software Stateflow Model
Code generated from the Software Stateflow Model Version 1.0