Closed-Loop Formal Verification of ICDs Using Cardiac Electrophysiological Models

植入式心脏除颤器（ICD）处于预防室性心律失常患者猝死的最前沿。 ICD已经发展成复杂的信息物理系统（CPS），其紧密地感测、硬件和软件以基于电描记图信号诊断心律失常并控制心脏兴奋。这些设备是生命攸关的，但用于确定其安全性的验证和确认（V V）技术仍然有些非正式，并在很大程度上依赖于广泛的单元测试。在形式验证技术方面有许多令人兴奋的发展。本提案将这些技术引入ICD验证过程，并将证明其适用于其他医疗器械。该项目将为ICD开发基于模型的框架，并将正式验证技术（如模型检查和可达性分析）应用于高保真心脏电生理模型，这些模型捕获ICD控制软件诱导的电激励。 通过与FDA研究人员的广泛合作，该提案将证明正式验证技术的有效性和在医疗器械应用中的适用性。

Implantable Cardiac Defibrillators (ICDs) are at the forefront of preventing sudden death in patients suffering from ventricular arrhythmias. ICDs have evolved into complex Cyber-Physical Systems (CPS)which tightly sensing, hardware, and software to diagnose arrythmias based on electrogram signals and control cardiac excitation. These devices are life-critical, yet the Verification and Validation (V&V) techniques used for establishing their safety have remained somewhat informal, and rely largely on extensive unit testing. There have been a number of exciting developments in formal verification technologies. This proposal introduces these techniques into the ICD verification process, and will demonstrate their suitability for application in other medical devices. The project will develop a model-based framework for ICDs, and will apply formal verification techniques, such as model checking and reachability analysis, to high-fidelity cardiac electrophysiological models that capture the electrical excitation induced by the ICD's control software. Through extensive collaboration with FDA research staff, the proposal will demonstrate the effectiveness of formal verification technology and suitability in medical device applications.