The hemodialysis machine case study

Authors Atif Mashkoor
Editors Michael Butler
Klaus-Dieter Schewe
Atif Mashkoor
Miklós Biró
Title The hemodialysis machine case study
Booktitle Abstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2016
Type in proceedings
Publisher Springer
Series Lecture Notes in Computer Science
Volume 9676
ISBN 978-3-319-33599-5
DOI 10.1007/978-3-319-33600-8_29
Month May
Year 2016
Pages 329-343
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.