The human heart maintains blood circulation of the body by contraction of the atria and ventricles. A special tissue in the Sinus node generates the electrical signal which is the primary pacemaker of the heart. The Sinus node spontaneously produces an electrical signal, which is conducted through Internodal pathways into the atrium causing its contraction. The signal then passes through the slow conducting atrioventricular (A-V) node, allowing the blood to empty out the atria and fill the ventricles. The fast conducting His-Purkinje system spreads the electricity through the ventricles, causing all tissues in both ventricles to contract simultaneously and to force blood out of the heart. This electrical system is the natural pacemaker of the heart. Abnormalities in the electrical signal generation and propagation can cause different types of arrhythmias such as Tachycardia and Bradycardia, which require medical intervention in the form of medication, surgery or implantable pacemakers. The heart normally has around 60-100 beats per minute and a heart beat is essentially a contraction of the ventricle. The electrical signal that passes through the heart is known as action potential. This is the signal that an implantable pacemaker will receive or generate. The action potential is triggered by a voltage spike from the action potential of its neighbouring tissue or from an artificial pacing signal. The upstroke indicates the depolarization of the cell and the time when the muscle contracts. This is followed by the plateau, which allows the muscle to hold its contraction and fully eject blood. The downstroke is repolarisation, when the muscle relaxes and refills.
Implantable cardiac pacemakers are the most commonly used cardiac rhythm management devices. The primary purpose of a pacemaker is to maintain an adequate heart rate through electrical impulses delivered to the heart. Nowadays, millions of implantable pacemakers are used worldwide. Because of safety-critical implications, they must be designed and programmed to the highest levels of safety and reliability. Unfortunately, according to the US Food and Drug Administration, errors in embedded software have led to a substantial increase in safety alerts, costly device recalls or even patient death. Combined with the relative lack of standardisation in the field of medical devices, there is an urgent need to develop methodologies for ensuring correct behaviour of embedded pacemaker software.
Embedded software is at the heart of cardiac pacemakers, and rigorous software design methodologies are needed to guarantee their safety and reliability. A major challenge for current verification methods is that pacemaker software cannot be analyzed in isolation, but in closed-loop with models of the human heart that are typically characterised by probabilistic and non-linear dynamics. We developed a model-based framework for the analysis and quantitative verification of closed-loop cardiac pacemakers based on hybrid and timed automata networks. Our techniques allow for quantitative verification of safety requirements and support the analysis of advanced pacing algorithms that rely on runtime data from physiological sensors. We also developed quantitative synthesis methods that enable automated design optimisation for pacemakers, in order to ensure energy efficency or derive safe and robust pacing therapies. With our framework, heart models can be personalised from electrocardiogram data, which is key for achieving more effective and patient-specific treatments.
To know more about these models and analysis techniques, follow the links below.Heart and pacemaker models » Analysis methods and tools »