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 …