The cardiac pacemaker is a rhythm management device that maintains the minimum heart rate and synchrony between its chambers, thereby improving the condition of patients with cardiac arrhythmias. Cardiac rhythm management devices have grown in complexity with over 80,000 to 100,000 lines of code. The primary approach to system-level testing of medical devices is unit testing using a playback of pre-recorded electrogram and electrocardiogram signals. This tests if the input signal triggers a particular response by the pacemaker but cannot evaluate if the response was appropriate for the patient condition. Furthermore, this approach of open loop "tape testing" is unable to check for safety violations due to inappropriate stimulus by the pacemaker. Pacemaker Mediated Tachycardia (PMT), a condition where the pacemaker inappropriately drives the intrinsic heart-rate toward the maximum rate, is a strong example of why we need an interactive and adaptive closed-loop verification and testing of such systems. With a tape test, PMT would not be observed and the response of the pacemaker could be classified as appropriate therapy.

Our proposed model-driven design (MDD) for Medical CPS begins with developing integrated functional and formal heart models that interact with real and modeled pacemakers for closed-loop verification and testing. The heart-pacemaker closed-loop systems is first modeled abstractly to facilitate verification of the basic pacemaker design with maximum coverage. In our case, we use timed automata and the UPPAAL model checker at this design stage. Next, the models are translated to more detailed models that take into account the complex dynamics of the heart and interaction with more detailed pacemaker model. We use Stateflow and Simulink at this design stage. These models are validated by physicians for their clinical relevance. The automatic model translation procedure, from UPPAAL to Stateflow, ensures that abstract models used for verification over-approximate the more detailed models used downstream. Once the detailed models pass simulation-based testing with closed-loop dynamics, they are automatically generated into code and are subject to platform-level integration testing. This MDD approach ensures the closed-loop safety properties are retained through the design toolchain and facilitates the development of verified software from verified models. <Back to Top>

Furthermore, they are primarily concerned with the mechanics of fluid flow, take several hours to simulate one QRS interval (heart beat) and do not interact with medical devices. We are interested in the heart's electrophysiological function which is responsible for its coordinated contraction and rhythmic operation.
In order to test and verify a closed-loop heart-pacemaker system, we had to design a series of heart models that (a) functionally express correct electrophysiological behavior of a functioning (i.e. normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart, as expected by the pacemaker, (b) are formally structured to interface with both modeled and real pacemakers such that the timing of all activity is verifiable by model checking tools, and (c) operate in real-time and expose electrical signals with any real pacemaker for platform-level testing. Given these requirements, we designed a Real-Time Virtual Heart Model (VHM) as network of timed-automata representing the timing and propagation of electrical signals.

These models enable high-fidelity system simulation, taking real system dynamics into account, in order to validate the initial assumptions used in the verification stage. Similarly, during the validation procedure, it was necessary to \emph{ensure equivalence} between the controller models used for verification and simulation. Therefore, in this process we provided guarantees that the properties verified in the early stage were still satisfied, as the system model was refined. Finally, the verified model must be translated into executable code for physical implementation, which is then validated using different testing procedures based on the initial system specification.

We developed a MDD framework ensuring successive models are consistent through the development process:
(a) a timed-automata based UPPAAL model and model verification of the controller software;
(b) automatic translation of the model to Stateflow using the UPP2SF tool developed by us;
(c) testing of the Stateflow model; and
(d) automatic modular code generation, test generation and testing of timing errors on hardware platforms.

We developed the UPP2SF tool for automatic conversion of verified models (in UPPAAL) to Simulink/ Stateflow for simulation. Using Simulink's support for code generation, this allows for automatic end-to-end model translation across multiple levels of abstraction, to modular code synthesis.

For example, one large randomized trial compared patients with default pacemaker algorithms and those with reduced pacing, showed a 54% increase for heart failure occurs with a 10\% increasing cumulative ventricular pacing. Given their association with an increased risk for heart failure and possibly death, several advances aimed at minimizing over-pacing are been explored including changes in atrioventricular pacing algorithms, novel pacing mode modifications, and better identification of hemodynamically optimal pacing sites. Recently, Medtronic introduced Managed Ventricular Pacing and Sorin/ELA introduced AAIsafeR, aimed to reduce ventricular pacing as much as possible. By reducing pacing to 10% to 19% of default ventricular pacing, patients exhibited significantly lower event rates. Thus, in order to fairly evaluate the performance of pacemaker, it is not enough to verify YES/NO safety properties. Quantitative verification provides us with the capability to evaluate pacemaker performance according to some cost functions and results in comparable numbers. With quantative verification we can answer questions such as "What is the probability that a particular pacing algorithm results in ventricular dissynchrony?" and "How can the probability of a particular arrhythmia be reduced?" The need for finer, probabilistic analysis will also require probabilistic extensions to our heart and patient models. Learn more >

However, to reduce the burden on caregivers and the overall health-care costs, it is necessary to guarantee safety and effectiveness of interoperating medical devices. The main challenges in these closed-loop scenarios are insufficient understanding of the human body's response to treatment, and the high degree of parametric uncertainty and variability between patients. To study effects of the medical device interconnectivity and interoperability with network-enabled control on the patient safety, we have considered a closed-loop clinical scenario: a system for the physiologic closed-loop control of drug infusion. The main contribution of our work is the verification approach for the safety properties of closed-loop medical systems. Our method combines robust-control techniques and simulation-based analysis of a detailed model of the system (including continuous-time patient dynamics with uncertain parameters) with model checking of a more abstract timed-automata model. We have shown that the relationship between the two models preserves the crucial aspect of the timing behavior, thus, ensuring the conservativeness of the safety analysis. We also describe a system design that can guarantee open-loop safety under network failure.

test

test