Report 18: Formalizing Insulin Pump using Event-B

Research Area: McSCert Reports Year: 2014
Type of Publication: Technical Report Keywords: Insulin Infusion Pump, IIP, Event-B, refinement, formal methods, verification, validation
  • Neeraj Kumar Singh
  • Hao Wang
  • Mark Lawford
  • Thomas S. E. Maibaum
  • Alan Wassyng
An insulin infusion pump (IIP) is a critical embedded medical device that infuses insulin satisfying patient needs under the safety and timing constraints for diabetes treatment. This device is used by millions of people around the world. The USA Food and Drug Administration (FDA) has reported several recalls that IIP failures are responsible for a large number of serious illnesses and deaths. The failures are caused by introducing hardware or software design errors during the system development process. This paper presents an incremental proof-based development of an IIP, where system requirements are already described into tabular expressions. 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.