The hemodialysis machine case study

Autoren Atif Mashkoor
Editoren Michael Butler
Klaus-Dieter Schewe
Atif Mashkoor
Miklós Biró
TitelThe hemodialysis machine case study
BuchtitelAbstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2016
Typin Konferenzband
SerieLecture Notes in Computer Science
SCCH ID#1542

This document presents a description of a case study concerning the control of a hemodialysis (HD) machine. It provides an overview of the requirements and the design of an HD machine including a sketch of the machine's functionality, related safety conditions, and a top-level system architectural description. This case study is supposed to stimulate research and pedagogical activities related to the use of formal methods in a medical application domain with challenging requirements concerning safety and hardware/software interaction.

Kidney diseases are becoming endemic in recent times. There are several contributing factors such as changed life style as well as increase in hypertension and diabetes. Kidneys are the organs that are responsible for cleaning human blood by removing excess fluid, minerals and wastes. They also aid regulating blood pressure, electrolyte balance, and red blood cell production. When kidneys fail, toxic waste products are accumulated in the human body, causing a rise in blood pressure and a decline in the production of red blood cells. When kidneys fail completely, an artifcial system is required that can substitute their functionality.

Hemodialysis (HD) is a treatment for kidney failure that uses a machine to send the patient's blood through a filter, called a dialyzer, for extracorporeal removal of waste products. The blood is transported to and from the patient's body through a surgically created vein during this process. The blood then travels through a tube that takes it to the dialyzer. Inside the dialyzer, the blood flows through thin fibers that filter out wastes and extra fluid. The machine returns the filtered blood to the body through a different tube. A vascular access lets large amounts of blood flow continuously during HD treatments to filter as much blood as possible per treatment. A specific amount of blood (approx. a pint) is conducted through the machine every minute.

This document is structured as follows: Section 2 presents a high-level architectural description of the HD machine describing its main components. Section 3 gives an overview of different types of dialysis therapies and how a therapy is conducted. Finally, Section 4 lists several general and software safety requirements related to the correct operation of the HD machine.