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.

A number of structural coverage criteria have been proposed to measure the adequacy of testing efforts. In the avionics and other critical systems domains, test suites satisfying structural coverage criteria are mandated by standards. With the advent of powerful automated test generation tools, it is tempting to simply generate test inputs to satisfy these structural coverage criteria. However, while techniques to produce coverage-providing tests are well established, the effectiveness of such approaches in terms of fault detection ability has not been adequately studied. In this work, we evaluate the effectiveness of test suites generated to satisfy four coverage criteria through counterexample-based test generation and a random generation approach-where tests are randomly generated until coverage is achieved-contrasted against purely random test suites of equal size. Our results yield three key conclusions. First, coverage criteria satisfaction alone can be a poor indication of fault finding effectiveness, with inconsistent results between the seven case examples (and random test suites of equal size often providing similar-or even higher-levels of fault finding). Second, the use of structural coverage as a supplement-rather than a target-for test generation can have a positive impact, with random test suites reduced to a coverage-providing subset detecting up to 13.5 percent more faults than test suites generated specifically to achieve coverage. Finally, Observable MC/DC, a criterion designed to account for program structure and the selection of the test oracle, can-in part-address the failings of traditional structural coverage criteria, allowing for the generation of test suites achieving higher levels of fault detection than random test suites of equal size. These observations point to risks inherent in the increase in test automation in critical systems, and the need for more research in how coverage criteria, test generation approaches, the test oracle use- , and system structure jointly influence test effectiveness.

The oracle - a judge of the correctness of the system under test (SUT) - is a major component of the testing process. Specifying test oracles is challenging for some domains, such as real-time embedded systems, where small changes in timing or sensory input may cause large behavioral differences. Models of such systems, often built for analysis and simulation, are appealing for reuse as oracles. These models, however, typically represent an idealized system, abstracting away certain issues such as non-deterministic timing behavior and sensor noise. Thus, even with the same inputs, the model’s behavior may fail to match an acceptable behavior of the SUT, leading to many false positives reported by the oracle.We propose an automated steering framework that can adjust the behavior of the model to better match the behavior of the SUT to reduce the rate of false positives. This model steering is limited by a set of constraints (defining acceptable differences in behavior) and is based on a search process attempting to minimize a dissimilarity metric. This framework allows non-deterministic, but bounded, behavior differences, while preventing future mismatches, by guiding the oracle-within limits-to match the execution of the SUT. Results show that steering significantly increases SUT-oracle conformance with minimal masking of real faults and, thus, has significant potential for reducing false positives and, consequently, development costs.