An event-b approach to timing issues applied to the generic insulin infusion pump

An insulin infusion pump (IIP) is a complicated and time critical control system. Making sure that the pump infuses insulin in conformance with a user's wishes and in conformance with safety related constraints, and does so at the right times, makes it a highly safety critical system. This paper uses Event-B to specify a generic model for an IIP, based on requirements developed by the US Food and Drug Administration (FDA). The IIP is an active and reactive control system. Each transition between states of the model is modelled as an event. To correctly specify the IIP, we need a model of time and synchronization of events with time that is sufficiently rich to achieve our safety aims. We create several sets to model the activation times of different events and the union of these time sets defines a global time activation set. All the actions in an event are triggered only when the global time matches the time specified in the event. When the action is activated, the time is deleted from the corresponding time set, but not the corresponding global time set. A time point is deleted from the global time set only when there are no pending actions for that time point. We are able to demonstrate that the resulting specification satisfies relevant required safety constraints.