Case studies
Insulin pump
Internet worm
Ariane 5
Airbus
London Ambulance
 
  Case study : The automated insulin pump

System overview
Diabetes is a medical condition where the body does not manufacture its own insulin. Insulin is used to metabolise sugar and, if it is not available, the person suffering from diabetes will eventually be poisoned by the build-up of sugar. It is important to maintain blood sugar levels within a safe range as high levels of blood sugar have long-term complications such as kidney damage and eye damage. These are not however, normally dangerous in the short-term.

Very low levels of blood sugar (hypoglaecemia) are potentially very dangerous in the short-term. They result in a shortage of sugar to the brain which causes confusion and ultimately a diabetic coma and death. In such circumstances, it is important for the diabetic to eat something to increase their blood sugar level.

Most diabetics are currently treated by injections of insulin 2 or 3 times a day but this leads to peaks and troughs in their level of insulin. A portable insulin pump measures the level of blood sugar at regular intervals and delivers doses of insulin depending on the actual level of sugar in the blood. This will lead to a situation where the sufferer’s blood sugar levels are much closer to those of people without diabetes. The complications and long-term effects of diabetes can therefore be reduced.

The system measures the level of blood sugar every 10 minutes and if this level is above a certain value and is increasing then the dose of insulin to counteract the increase is computed and injected into the diabetic. The system can also detect abnormally low levels of blood sugar and, if these occur, an alarm is sounded to warn the diabetic that they should take some action.

This case study focuses on the control software for the insulin pump which is concerned with reading the blood sugar (glucose) sensor, computing the insulin requirements and controlling the micro pump which causes the insulin to be delivered.

 

Description

This case study is used throughout the book to illustrate various aspects of embedded critical systems including specification and safety analysis. The material here is based on classwork that I set around this system where students had to write a simulation of it.

General overview of the system

Use in teaching

You can use the material here to illustrate dependability specification, the use of formal specification in critical systems engineering and issues of critical systems validation.

Related chapters

Chapter 3: Dependability
Chapter 9: Critical systems specification
Chapter 10: Formal specification
Chapter 20: Critical systems development
Chapter 24: Critical systems validation

Supporting documents

A commercially available blood sugar meter and injection device.

Coursework description     Sets out what students are expected to do.

Requirements specification   Describes the user requirements for the insulin pump. Makes references to the formal specification to describe how the sugar levels are computed from the insulin levels. Should be supplemented with formal specification and associated presentations:

Insulin pump overview (Powerpoint slides and notes. Describes the general operation and how insulin dose is computed)

Insulin pump dependability specification (Discusses the derivation of dependability requirements for the insulin pump)

Insulin pump validation (Discusses the validation of the safety of the pump)

Formal Specification in Z     This is a formal specification for the insulin pump control software written in the Z specification language. The only aspect of the system that is not formally specified is the timing which is (in my view) very unnatural to do in Z. To understand this, you need an elementary knowledge of Z - not any of the more advanced features.

This is NOT a formal specification of the simulator for the pump, only for the control software.

The following code and manuals were developed by Ben McCarthy, a student at Lancaster who took my course in 2001-2002. Ben has done one of the best projects that I have seen. Thanks to Ben for making this code and documents available.

Java code for the simulator    This is a zip file containing the Java classes to implement the simulator.

Simulator system design document. Discusses the overall design of the simulation system

Simulator user manual    A user manual for the simulation system.

 
 
  
The material here has been included for its instructional value. Neither the author nor Pearson Education Ltd offer any warranties or representations in respect of its fitness for a particular purpose. No liability is accepted by either the author or the publisher for any loss or damage arising from its use.  The dynamic nature of the web means that it cannot be guaranteed that all links will work. Please let me know of broken links and I will try and fix them.