|An embedded insulin pump|
|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.
Use in teachingYou can use the material here to illustrate dependability specification, the use of formal specification in critical systems engineering and issues of critical systems validation.
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.