License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.MCPS.2014.137
URN: urn:nbn:de:0030-drops-45317
Go to the corresponding OASIcs Volume Portal

Kwiatkowska, Marta ; Mereacre, Alexandru

Automated Verification of Quantitative Properties of Cardiac Pacemaker Software

16.pdf (0.5 MB)


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.

BibTeX - Entry

  author =	{Marta Kwiatkowska and Alexandru Mereacre},
  title =	{{Automated Verification of Quantitative Properties of Cardiac Pacemaker Software}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{137--140},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Volker Turau and Marta Kwiatkowska and Rahul Mangharam and Christoph Weyer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-45317},
  doi =		{10.4230/OASIcs.MCPS.2014.137},
  annote =	{Keywords: Pacemakers, Verification, Simulink}

Keywords: Pacemakers, Verification, Simulink
Collection: 5th Workshop on Medical Cyber-Physical Systems
Issue Date: 2014
Date of publication: 14.04.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI