Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements

An insulin infusion pump (IIP) is a critical software-intensive medical device that infuses insulin satisfying patient needs under safety and timing constraints that are appropriate for the treatment of diabetes. This device is used by millions of people around the world. The USA Food and Drug Administration (FDA) has reported several recalls in which IIP failures were responsible for a large number of serious illnesses and deaths. The failures responsible for this harm to people who are dependent on external insulin were caused by the introduction of hardware or software design errors during the system development process. This paper presents an incremental proof-based development of an IIP. We use the Event-B modelling language to formalize the given system requirements. Further, the Rodin proof tools are used to verify the correctness of functional behaviour, internal consistency checking with respect to safety properties, invariants and events.