An embedded insulin pump
Case studies
Insulin pump
Internet worm
Ariane 5
Airbus FCS
London Ambulance
SE 8 Web


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.