The human body creates metabolic waste products like urea and minerals. Usually, the kidneys are responsible for the removal of these waste products from the blood, but when they fail, a hemodialysis machine can be used for this removal process instead. Such a machine has a direct influence on the chemical composition of a patient's blood and thus is a safety-critical system. The case study was originally introduced for ABZ 2016.

The S# version of the case study can be found here.

A conceptual overview of a hemodialysis machine connected to a patient is shown above. It consists of three parts: The extracorporeal blood circuit, the dialyzer, and the dialyzing fluid delivery system. The patient's artery and vein are connected to the extracorporeal blood circuit through syringes. The main purpose of the extracorporeal blood circuit is to deliver the blood from the patient to the dialyzer and subsequently back again to the patient once it has been cleaned of the metabolic waste products. The blood pump pumps the patient's blood through the extracorporeal blood circuit with the heparin pump adding heparin into the patient's blood to prevent blood clotting. The arterial and venous pressure transducers monitor blood pressure values while the arterial and venous chambers decrease the amount of gas in the blood. The venous tubing valve is a safety measure that prevents contaminated blood from reentering the patient: Whenever the safety detector detects contaminated blood or gas in the blood, the venous tubing valve is closed so that no blood can enter the patient.

The dialyzer itself is part of two fluid flows: The blood flow of extracorporeal blood circuit and a dialyzing fluid flow of the dialyzing fluid delivery system. Inside the dialyzer, these two flows are separated by a semipermeable membrane through which waste products diffuse from the blood into the dialyzing fluid. The incoming dialyzing fluid of the dialyzer is produced by the dialyzing fluid delivery system: Water is heated up to body temperature and mixed with dialyzing fluid concentrate until it reaches the appropriate chemical composition. The balance chamber acts as a buffer for the dialyzing fluid to ensure proper application. The safety bypass ensures that dialyzing fluid of unacceptable temperature is piped to the drain so that it does not reach the the dialyzer; red blood cells could burst when the fluid is too warm or the patient's blood would become too cold if the dialyzer fluid is not warm enough. Finally, the ultrafiltration pump and the pump to the balance chamber establish the flow of the dialyzing fluid.

Nine faults are considered in hemodialysis machine case study: The blood pump of the extracorporeal blood circuit does not create suction. The pump that pumps the fresh dialyzing fluid to the balance chamber might not create any suction towards the water supply. Moreover, the pump pumping the dialyzing fluid from the dialyzer back to the balance chamber might fail , or the ultrafiltration pump might be defect. The membrane of the dialyzer might rupture so that the dialyzing fluid inside the dialyzer gets contaminated by blood and the chemical composition of the blood inside the dialyzer gets disordered. The safety bypass cannot pipe the dialyzing fluid into the drain anymore, causing it to forward all dialyzing fluid into the dialyzer, even if the dialyzing fluid does not meet the temperature constraints. The water preparation might not heat the incoming water anymore. The safety detector might not detect contaminated blood and even if it does, the venous tubing valve might be unable to be closed.

The hemodialysis machine is used to cleanse a patient's blood from metabolic waste products. Consequently, a hazard occurs when the device fails to do so for various reasons related to occurrences of one or more of the aforementioned faults, that is, dialysis is unsuccessful when the overall dialyzing process is completed but the patient's blood is still not fully cleaned. Additionally, there is the hazard of contaminated blood entering the patient which the safety detector and the venous tubing valve are designed to prevent. But like all safety measures, they can fail, resulting in potentially lethal doses of contaminated blood being pumped into the patient.

The case study consists of a multitude of different components connected together through fluid flows. In order to facilitate formal safety analysis, these flows must be represented in a model, abstracting from the underlying complex physical laws in order to conduct qualitative safety analyses without taking all physical details into account. The main challenge therefore lies in a systematic and modular modeling approach to create a comprehensive model that allows for formal safety analyses.