From Verified Models to Verified Code for Medical Devices

Abstract:

The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs who's response is not fully understood. Safety recalls of pacemakers and implantable cardioverter defibrillators between 1990 and 2000 affected over 600,000 devices. Of these, 200,000 or 41%, were due to firmware issues (i.e. software) that continue to increase in frequency [1]. There is currently no formal methodology or open experimental platform to test and verify the correct operation of medical device software within the closed-loop context of the patient. The goal of this proposal is to develop the foundations of modeling, synthesis and development of verified medical device software and systems from verified closed-loop models of the device and organ(s). The proposed research spans both implantable medical devices such as cardiac pacemakers and physiological control systems such as drug infusion pumps which have multiple networked medical systems. In both cases, the devices are physically connected to the body and exert direct control over the physiology and safety of the patient. Even though devices such as the pacemaker contain over 80,000 lines of code, the US Food and Drug Administration (FDA) currently does not inspect a single line of code nor requires explicit guarantees of the safety and correctness of the device software. While the onus of determining the safety of the software is largely with the manufacturers, they generally resort to open-loop testing. With open-loop testing, one can determine how the device responds to the state of the patient but cannot evaluate how the device drives the patient into unsafe states. For example, with Pacemaker Mediated Tachycardia, the pacemaker drives the heart to an unsafe state - a phenomenon can only be captured in closed-loop testing of device and organ. Intellectual Merit: The objective of our proposal is to develop the scientific foundation for modeling, verification, synthesis, testing and optimization of safe software for Medical Cyber-Physical Systems. We focus on the safety of medical devices with the patient-in-the-loop and ensure the device will never drive the patient into an unsafe state while providing effective therapy. The proposer's long term career goal is to develop the foundations for model- driven development (MDD) of Medical Cyber-Physical Systems so code generated from verified models is safe and efficient with closed-loop operation of the patient. The contributions of this proposal are as follows:

1. Integrated Functional and Formal Device-Patient Modeling: The key innovation of this theme is the development of a common kernel which produces both the "functional" physiological signals, that are clinically-relevant for interacting with the real device, and also generates the "formal" timing of device-patient interaction for formal verification. This allows for physiologically relevant testing and verification.
2. Quantitative Verification for Optimized Patient-specific Devices: While the focus so far has been on verifying the safety and correctness of the medical device software, our ultimate goal is to maintain the efficiency of the patient and the device. Using probabilistic patient models based on physiological data, quantitative verification techniques will be developed for the efficacy of therapy and energy costs. This facilitates competitive algorithm design at an early stage, parameter optimization of over 400+ pacemaker parameters for the patient and extends our understanding of model refinement for life-critical systems.
3. Platforms for Life-Critical Systems: The problems considered here are both ambitious and challenging and therefore require the participation of the CPS community, FDA, physicians and manufacturers. To facilitate this, we are developing open source libraries of device/patient models, software tools for verification and model translation and hardware platforms for testing with real medical devices, and contribute to the Formal Methods Pacemaker Grand Challenge [2, 3].

Educational Impact: Our proposed solution to this educational challenge is that everyone views everything as a system. We incorporate this philosophy in the newly formed Masters in Embedded Systems, a first in our nation. We will develop three domain-specific CPS courses covering Life-Critical Computing, Networked and Embedded Control Systems, and Medical CPS. Open source tools and test-beds will be available via the CPS-VO.

Broader Impact: Closed-loop design and verification techniques will significantly improve patient safety, reducing the burden on caregivers and the overall costs of health care. The scientific agenda is to unify theories of formal methods, control of physiological systems, communication and computing systems