From verified models to verified code for safe medical devices

Medical devices play an essential role in the care of patients around the world, and can have a life-saving effect. An emerging category of autonomous medical devices like implantable pacemakers and implantable cardioverter defibrillators (ICD) diagnose conditions of the patient and autonomously deliver therapies. Without trained professionals in the loop, the software component of autonomous medical devices is responsible for making critical therapeutic decisions, which pose a new set of challenges to guarantee patient safety. As regulation effort to guarantee patient safety, device manufacturers are required to submit evidence for the safety and efficacy of the medical devices before they can be released to the market. Due to the closed-loop interaction between the device and the patient, the safety and efficacy of autonomous medical devices must ultimately be evaluated within their physiological context. Currently the primary closed-loop validation of medical devices is in form of clinical trials, in which the devices are evaluated on real patients. Clinical trials are expensive and expose the patients to risks associated with untested devices. Clinical trials are also conducted after device development, therefore issues found during clinical trials are expensive to fix. There is urgent need for closed-loop validation of autonomous medical devices before the devices are used in clinical trials. In this thesis, I used implantable cardiac devices to demonstrate the applications of model-based approaches during and after device development to provide confidence towards the safety and efficacy of the devices. A heart model structure is developed to mimic the electrical behaviors of the heart in various heart conditions. The heart models created with the model structure are capable of interacting with implantable cardiac devices in closed-loop and can provide physiological interpretations for a large variety of heart conditions. With the heart models, I demonstrated that closed-loop model checking is capable of identifying known and unknown safety violations within the pacemaker design. More importantly, I developed a framework to choose the most appropriate heart models to cover physiological conditions that the pacemaker may encounter, and provide physiological context to counter-examples returned by the model checker. A model translation tool UPP2SF is then developed to translate the pacemaker design in UPPAAL to Stateflow, and automatically generated to C code. The automated and rigorous translation ensures that the properties verified during model checking still hold in the implementation, which justifies the model checking effort. Finally, the devices are evaluated with a virtual patient cohort consists of a large number of heart models before evaluated in clinical trials. These in-silico pre-clinical trials provide useful insights which can be used to increase the success rate of a clinical trial. The work in this dissertation demonstrated the importance and challenges to represent physiological behaviors during closed-loop validation of autonomous medical devices, and demonstrated the capability of model-based approaches to provide safety and efficacy evidence during and after device development