Problem Statement
-
Over 600,000 cardiac medical devices recalled from 1990-2000.
40% of recent recalls were due to software issues
It is essential to guarantee the safety and efficacy of the device software
-
The Pacemaker (and other medical devices):
- Autonomous device with minimum human interaction, therefore has to be able to operate under all possible conditions.
- Limited diagnostic capability, inevitably leading to false-positives and false-negatives, and limited therapy capability, being able to treat the disease to a certain degree.
- It is the safety of the patient we care about. Therefore the safety of the pacemaker must be evaluated in closed-loop within its environment
-
The physical plant:
- Not only the heart, but also the rest of the body
- Different dynamics even in a single patient
- Each condition has its own corresponding optimal condition
Currently the US FDA requires the device manufacturers to submit proofs for:
-
The final product: The safety and efficacy of the device itself
-
The development process: Rigorous design process which provides traceability of requirements
In traditionally software development, the domain experts first specify safety/efficacy requirements for the software. Together with a software engineer they agree on the software specification which is designed to address the requirements. Then together with an electrical engineer the specification is implemented on hardware. From the process we can see that the requirements, the specification and the implementation are 3 isolated documents and there is no formal proof to claim that the final implementation satisfies all the requirements. This is definitely a problem during FDA certification.
We developed a model based design framework which ensures the safety and efficacy of the pacemaker software. The software specification of the pacemaker software is first represented by a model. Together with the heart model we developed, the closed-loop system can be verified against safety/efficacy properties using Model Checking This process ensures that the specification is able to satisfy the requirements
Pacemaker Modeling
A dual chamber pacemaker has 5 basic timing cycles which do the following things
-
Maintain lowest ventricular rate and highest paced ventricular rate to keep adquate and efficient blood supply.
- Maintain appropriate A-V interval to ensure optimal stroke volume.
- Filter physiologically-infeasible signals as noises which may disrupt normal pacemaker functions.
An example of the 5 timers are shown below:
In model checker UPPAAL, we modeled each timing cycle as a component and they communicate with broadcast channels. The UPPAAL model of the 5 timing cycles are shown below:
For evaluating pacemaker which has only two leads and do simple thresholding for signal processing, we developed heart models at different abstraction levels, where each abstraction covers all possible states of the model in the previous abstraction level. Each abstraction step reduces the complexity of the timed automata component and/or the structure of the whole model. This establishes a timed simulation relationship between abstraction levels with 
where n=[1,4]. More details on heart model abstraction can be found in our STTT paper.
Behaviorial Model of Heart Tissue
We first start with modeling the electrical behaviors of a heart tissue. A whole model of the heart consists of node automata (N0) which models the timed transitions among different time periods with different behaviors after the tissue is depolarized. The heart can then be modeled as: 
where N can be arbitarily large.
Proposed use:
- Study complex and chaotic heart conditions like Atrial Fibrillation.
- Creating spatial and temporal map of the heart during Electrophysiology Studies
Abstract conduction delay with paths
In this abstraction we replace the cond state of N0 with path automata. The heart model H0 can be replaced by 
. A more general abstraction abstracts 3 nodes and 2 paths into 2 nodes and 1 path:
. With this property we can further abstract the structure of the model. The heart model H0.5 can be further abstracted into 
where m=9 in the structure shown on the right.
Proposed use:
- Study heart conditions with additional pathways including reentry circuits.
- Patient-specific heart model for general Electrophysiology Study.
Merging equivalent states
At this abstraction level, we merge the RRP state with the Rest state in the node automata and Double with the Idle state in the path automata due to the same behavior. We also further abstract the structure of the heart model so H1 can be abstracted with 
. The AV node has very large ERP period thus cannot be abstracted away.
Proposed use:
Verify pacemaker algorithms in which the blocking property of the AV node cannot be ignored
Replacing the blocking property of ERP with non-determinism
The node automata do not trigger path conduction in response to external activation during its ERP state. In this abstraction level, this function is replaced by a non-determnistic transition in the path automata, as shown in the figure on the right. As a result of the abstraction, the AV node can be abstracted away and the heart model H2 can be abstracted by 
.
Proposed use:
Verify pacemaker algorithms in which A-V conduction cannot be ignored
Abstracting the conduction property with non-determinism
Since the pacemaker only has two leads, the structure of the heart model can be further reduced to two node automata which can generate inputs to the pacemaker without timing constraints. The heart model H3 can be further abstracted to 
. This heart model covers all possible inputs to the pacemaker and is our most abstracted model.
Proposed use:
Verify pacemaker algorithms with unconditional properties.
Basic Safety Properties
For model checking, we start from basic safety properties which should be satisfied by the pacemaker under all possible heart conditions. In this section, the most abstract heart model H4 which covers all possible heart inputs to the pacemaker, is the most suitable heart model to use.
The most intuitive unsafe states for the pacemaker is when the ventricular rate is too low or the pacemaker is pacing the ventricles too fast. The two monitors PLRI_test and PURI_test which helps property specification is shown below:
The property for the Lower Rate Limit is 
and the property for the Upper Rate Limit is 
. Our verification results shows that the basic dual chamber pacemaker with 5 timing cycles satisfies both properties: 
and 
Safety Properties Regarding Unsafe Executions
Most of the time the unsafe behavior of the pacemaker cannot be identified as a single state, but as closed-loop executions over a period of time. In this section, we use 2 already idendified and studied unsafe executions: Endless loop Tachycardia (ELT), and Atrial Tachycardia Response (ATR), as case studied to show:
- How they can be identified using model checking.
- How to verify the correctness of corresponding termination algorithms.
- Most importantly, how to refine the heart model when the model does not have the expressiveness to distinguish the unsafe behavior from the rest.
The most intuitive unsafe states for the pacemaker is when the ventricular rate is too low or the pacemaker is pacing the ventricles too fast. The two monitors PLRI_test and PURI_test which helps property specification is shown below:
The most intuitive unsafe states for the pacemaker is when the ventricular rate is too low or the pacemaker is pacing the ventricles too fast. The two monitors PLRI_test and PURI_test which helps property specification is shown below:
The property for the Lower Rate Limit is and the property for the Upper Rate Limit is . Our verification results shows that the basic dual chamber pacemaker with 5 timing cycles satisfies both properties: and
The most intuitive unsafe states for the pacemaker is when the ventricular rate is too low or the pacemaker is pacing the ventricles too fast. The two monitors PLRI_test and PURI_test which helps property specification is shown below:
The property for the Lower Rate Limit is and the property for the Upper Rate Limit is . Our verification results shows that the basic dual chamber pacemaker with 5 timing cycles satisfies both properties: and
The most intuitive unsafe states for the pacemaker is when the ventricular rate is too low or the pacemaker is pacing the ventricles too fast. The two monitors PLRI_test and PURI_test which helps property specification is shown below:
The property for the Lower Rate Limit is and the property for the Upper Rate Limit is . Our verification results shows that the basic dual chamber pacemaker with 5 timing cycles satisfies both properties: and
