PACING

A pacemaker is a medical device that uses electrical impulses, delivered by electrodes contracting the heart muscles, to regulate the beating of the heart. The primary purpose of a pacemaker is to maintain an adequate heart rate, either because the heart's natural pacemaker is not fast enough, or there is a block in the heart's electrical conduction system. Modern pacemakers are externally programmable and allow the cardiologist to select the optimum pacing modes for individual patients. (https://en.wikipedia.org/wiki/Artificial_cardiac_pacemaker)

This package contains a model of the pacing behavior of the software of a pacemaker, developed using the following specification document: http://sqrl.mcmaster.ca/_SQRLDocuments/PACEMAKER.pdf This model only captures the VVI (ventricle paced, ventricle sensed, inhibited response) and DDD (dual chambers paced, dual chambers senses, tracking response) pacing modes. Included in this package is the model, a set of seeded mutants, and associated test inputs used for model-based testing research.

For more information on this model, please see: [1] Pacemaker Formal Methods Challenge: http://sqrl.mcmaster.ca/pacemaker.htm [2] Gregory Gay. Automated Steering of Model-Based Test Oracles to Admit Real Program Behaviors. Ph.D. Thesis, University of Minnesota, May 2015.