Formal methods improve safety of software in artificial organs
The Future of Safety for SaMD
Software EngineeringComputers and SocietyLogic in Computer Science
Summary
Software that controls artificial organs can fail in ways people did not expect, which can be very dangerous because these devices stay inside patients for a long time. The authors explain that formal verification, a precise mathematical checking method, can prove that the software works correctly in every possible situation allowed by its instructions. This approach is already used to keep railways, planes, and nuclear plants safe. The authors discuss how to use these methods step by step for artificial organs and what safety guarantees they provide.
What this means in practice
- •For medical device manufacturers: Integrate formal verification techniques into existing IEC 62304 software development lifecycle to better guarantee artificial organ software safety.
- •For railway control engineers: Adapt existing formal verification methods from rail safety systems to improve software safety in biomedical devices like artificial organs.
A position paper. It proposes an approach and reports no results.
Authors
Rhea Malhotra, Tanya Sharma, Krisha Patel, Satvika Sharma, Heena Purkait, Mehak Nehal Makhija, Aellison Cassimiro, Everett Hildenbrandt, Palina Tolmach, Jaidev Shastri
Abstract
An artificial organ carries failure consequences on the scale of an aircraft or a reactor, but the software driving it is rarely held to the same standard. Teams building them rely on testing, which only reaches the failure modes someone thought of in advance. In a pump or controller that runs inside a patient for months, the dangerous cases are the ones nobody anticipated. Formal verification closes that gap. Applied to the device's software, it proves the code meets its specification for every execution that specification allows, and where a proof fails, it returns the exact input sequence that breaks it. The same methods already protect rail, aviation, and nuclear control systems, and they extend the IEC 62304 lifecycle that a manufacturer already follows rather than replacing it. In this paper, we explore how to apply formal verification to artificial organs, stage by stage, and what each technique actually guarantees about the device.