Oxford logo
[KM14] M. Kwiatkowska and A. Mereacre. Automated Verification of Quantitative Properties of Cardiac Pacemaker Software. In Proc. 5th Workshop on Medical Cyber-Physical Systems, volume 36 of OpenAccess Series in Informatics, pages 137-140, Schloss Dagstuhl. 2014. [pdf] [bib]
Downloads:  pdf pdf (533 KB)  bib bib
Abstract. This poster paper reports on a model-based framework for software quality assurance for cardiac pacemakers developed in Simulink and described in [Chen/Diciolla/Kwiatkowska/Mereacre - Information&Computation, 2013]. A novel hybrid heart model is proposed that is suitable for quantitative verification of pacemakers. The heart model is formulated at the level of cardiac cells, can be adapted to patient data, and incorporates stochasticity. We validate the model by demonstrating that its composition with a pacemaker model can be used to check safety properties by means of approximate probabilistic verification.