A personal insulin pump

This case study discusses the control software for a personal insulin pump, which is used by diabetics to mimic the function of the pancreas and hence control the level of glucose (sugar) in their blood. The system hardware is illustrated schematically in the following diagram:

Insulin Pump Diagram


The level of blood sugar depends on what the system user has eaten, the speed of their digestive processes and the effectiveness of their body in metabolising blood sugar. Therefore, their is not a simple relationship between a blood sugar measurement and the amount of insulin to be injected. Rather, the control system has to make several measurements and assess the rate of change of blood sugar. Based on the current level and the rate and direction of change, the incremental amount of insulin to be injected is computed and injected using the micro-pump in the system. This is a safety-critical system as failure to inject the correct amount of insulin can have serious health consequences.

Use of this case study in teaching

I use this case study to discuss general issues of safety and safety-critical systems. It is used in discussing issues of dependability specification and the use of formal specification techniques in dependable system engineering. Formal specification is especially valuable for this system as the computation to calculate the amount of insulin required is detailed and complex and quite difficult to specify using natural language. The formal specification in the Z notation is here and I discuss the specification of the control algorithm in the web chapter on formal specification. In lectures on dependability assurance, I use examples from the insulin pump system to illustrate safety arguments and safety cases. You can use the example more generally in lectures on requirements engineering, system modeling and embedded systems.

Supporting documents

Overview of a software controlled insulin pump

System overview slides (PPTX)

Insulin Pump Requirements Specification (which references the formal specification so is not a stand-alone document).

Insulin Pump Z schemas