The Future of Safety for SaMD
TL;DR
This paper explores how to apply formal verification to artificial organs, stage by stage, and what each technique actually guarantees about the device.
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.
