发表机构
Fresenius Medical Care; Baxter Healthcare; Virginia Tech University（费森尤斯医疗; 百特医疗; 弗吉尼亚理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文探讨将形式化验证分阶段应用于人工器官软件，以弥补测试盲区，确保代码满足规范并扩展 IEC 62304 生命周期，提升 SaMD 安全性。
AI 中文摘要
人工器官在失效时带来的后果堪比飞机或反应堆，但驱动其运行的软件却很少被要求达到同样的标准。开发这些软件的团队依赖测试，而测试只能覆盖到事先有人想到的失效模式。对于在患者体内运行数月之久的泵或控制器，危险的案例往往是那些无人预料到的情况。形式化验证填补了这一空白。将其应用于设备软件，它可以证明代码在规范允许的每一次执行中都满足该规范；当证明失败时，它会返回导致失败的确切输入序列。同样的方法已用于保护铁路、航空和核控制系统，并且它们扩展了制造商已经在遵循的 IEC 62304 生命周期，而非取代它。在本文中，我们探讨如何分阶段将形式化验证应用于人工器官，以及每种技术实际能为设备提供何种保证。
英文摘要
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.
Comments9 pages, 1 figure
