« Overview
Human Heart. Electrical Conduction System.
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.
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.
Safety guarantees and design optimisation. Quantitative verification and synthesis.
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 »
Sort by: date, type, title
13 publications:
-
[CDKM13]
T. Chen, M. Diciolla, M. Kwiatkowska and A. Mereacre.
A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers.
In Proc. 16th International Conference on Hybrid Systems: Computation and Control (HSCC 2013), pages 131-136, ACM.
2013.
[pdf]
[bib]
-
[BKM+16]
B.Barbot, M. Kwiatkowska, A. Mereacre, and N. Paoletti.
Building Power Consumption Models from Executable Timed I/O Automata Specifications.
In 19th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2016). To appear.
2016.
[pdf]
[bib]
-
[BKM+15a]
B. Barbot, M. Kwiatkowska, A. Mereacre and N. Paoletti.
Estimation and verification of hybrid heart models for personalised medical and wearable devices.
In 13th International Conference on Computational Methods in Systems Biology (CMSB 2015), volume 9308 of LNCS, pages 3-7.
2015.
[pdf]
[bib]
-
[KLMP14]
M. Kwiatkowska, H. Lea-Banks, A. Mereacre and N. Paoletti.
Formal Modelling and Validation of Rate-Adaptive Pacemakers.
In Proc. IEEE International Conference on Healthcare Informatics.
2014.
[pdf]
[bib]
-
[BKM+15]
C. Barker, M. Kwiatkowska, A. Mereacre, N. Paoletti, A. Patane.
Hardware-in-the-loop simulation and energy optimization of cardiac pacemakers.
In 37th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC).
2015.
[pdf]
[bib]
-
[HFMMK14]
Z. Huang, C. Fan, A. Mereacre, S. Mitra and M. Kwiatkowska.
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells.
In Proc. 26th International Conference on Computer Aided Verification (CAV), volume 8559 of LNCS, pages 373-390, Springer.
2014.
[pdf]
[bib]
-
[KMP14]
M. Kwiatkowska, A. Mereacre, and N. Paoletti.
On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers.
In Proc. 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 8803 of LNCS, pages 365-384, Springer.
2014.
[pdf]
[bib]
-
[CDKM12b]
T. Chen, M. Diciolla, M. Kwiatkowska and A. Mereacre.
Quantitative Verification of Implantable Cardiac Pacemakers.
In Proc. 33rd IEEE Real-Time Systems Symposium (RTSS), pages 263-272, IEEE.
December 2012.
[pdf]
[bib]
-
[CDKM13c]
T. Chen, M. Diciolla, M. Kwiatkowska and A. Mereacre.
Quantitative Verification of Implantable Cardiac Pacemakers over Hybrid Heart Models.
Information and Computation, 236, pages pages 87-101, Elsevier.
August 2014.
[pdf]
[bib]
-
[Dic14]
M. Diciolla.
Quantitative Verification of Real-Time Properties with Application to Medical Devices.
Ph.D. thesis, Department of Computer Science, University of Oxford.
2014.
[pdf]
[bib]
-
[HFM+15]
Z. Huang, C. Fan, A. Mereacre, S. Mitra, M. Kwiatkowska.
Simulation-based Verification of Cardiac Pacemakers with Guaranteed Coverage.
Design Test, IEEE, 32(5), pages 27 - 34, IEEE.
June 2015.
[bib]
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7130608
-
[DKKM14]
M. Diciolla, C. H. P. Kim, M. Kwiatkowska and A. Mereacre.
Synthesising Optimal Timing Delays for Timed I/O Automata.
In Proc. 14th International Conference on Embedded Software (EMSOFT'14), ACM.
2014.
[pdf]
[bib]
-
[KMP+15]
M. Kwiatkowska, A. Mereacre, N. Paoletti, A. Patane.
Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques.
In Proceedings of the 4th International Workshop on Hybrid Systems and Biology (HSB 2015), pages 119-140, Springer International Publishing.
January 2015.
[pdf]
[bib]
Sort by: date, type, title
« Overview