Formalizing the Glucose Homeostasis Mechanism

The failure of hardware or software in the medical domain can lead to injuries and loss of life. Design errors are a major source of the defects that are introduced during the system development process. Traditional validation and verification techniques such as simulation and testing are effective methods for detecting these defects, but are seriously limited in that they cannot guarantee to find all existing defects. Formal methods provide a complementary alternative to testing and simulation, and, although we do not yet have a ‘theory of coverage’ when combining formal validation and verification techniques with testing and simulation, the combination provides better coverage than any one of them on its own. The insulin infusion pump (IIP) is a critical system that is used by millions of people around the world. IIP failures are responsible for a large number of serious illnesses and deaths. This paper presents the formalization of the glucose homeostasis mechanism that provides an environmental model for the IIP. We can then use this model to validate the appropriateness and correctness of system behaviours at an early stage of development.