Towards the Trustworthy Development of Active Medical Devices: A Hemodialysis Case Study
This addresses safety-critical software failures in medical devices like hemodialysis machines, with potential generalization to other active devices, but it is incremental as it builds on existing formal methods.
The authors tackled the problem of software faults in active medical devices by developing a correct-by-construction approach for hemodialysis machines, demonstrating how informal requirements are modeled and analyzed to ensure trustworthiness.
The use of embedded software is advancing in modern medical devices, so does its capabilities and complexity. This paradigm shift brings many challenges such as an increased rate of medical device failures due to software faults. In this letter, we present a rigorous correct by construction approach for the trustworthy development of hemodialysis machines, a sub-class of active medical devices. We show how informal requirements of hemodialysis machines are modeled and analyzed through a rigorous process and suggest a generalization to a larger class of active medical devices.