Content Frame
Skip Breadcrumb Navigation
Home  arrow Student Resources  arrow Case studies  arrow The automated insulin pump

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.


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 Ian Sommerville has set around this system where students had to write a simulation of it.

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 Ian Sommerville's 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 Ian Sommerville's course in 2001-2002. Ian Sommerville states that this is one of the best projects he has ever 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.

Pearson Education Copyright © 1995-2006 Pearson Education. All rights reserved.
Legal and Privacy Notice

Return to the Top of this Page