Pacing

URL

Change Log

When What
September 21st, 2015 Donated by Gregory Gay

Reference

Studies who have been using the data (in any form) are required to include the following reference:

@misc{pacing
author = {Gregory Gay, Sanjai Rayadurgam, Mats Heimdahl },
title = {Pacing Model and Testing Data},
howpublished= {\url{http://crisys.cs.umn.edu/PublicDatasets.shtml}}

@inproceedings{Gay:2014:SMO:2591062.2591120,
 author = {Gay, Gregory and Rayadurgam, Sanjai and Heimdahl, Mats P. E.},
 title = {Steering Model-based Oracles to Admit Real Program Behaviors},
 booktitle = {Companion Proceedings of the 36th International Conference on Software Engineering},
 series = {ICSE Companion 2014},
 year = {2014},
 isbn = {978-1-4503-2768-8},
 location = {Hyderabad, India},
 pages = {428--431},
 numpages = {4},
 url = {http://doi.acm.org/10.1145/2591062.2591120},
 doi = {10.1145/2591062.2591120},
 acmid = {2591120},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Model-Based Testing, Software Testing, Test Oracles},
}

About the Data

Overview of Data

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.

Attribute Information

This package contains the following data:

/docs
	Papers where these models are described or used.
/models
	/stateflow
		The original model, developed in the Stateflow notation.
		/faulty
		A version of the model with real faults (see faults.docx in the docs folder)
	/lustre
		Model translated into the text-based Lustre modeling language.
		/faulty
		/mutants
		Mutated versions of the original model, used for fault-finding experiments.
/tests
	Test cases that satisfy various structural coverage metrics and
	randomly-generated test cases.
	Format is:
	input1,input2,…,inputN
	value_test1_step1,value_test1_step1,…,value_test1_step1

Paper Abstract

The oracle—an arbiter of correctness of the system under test (SUT)—is a major component of the testing process. Specifying oracles is particularly challenging for real-time embedded systems, where small changes in time or sensor inputs may cause large differences in behavior. Behavioral models of such systems, often built for analysis and simulation purposes, are naturally appealing for reuse as oracles. However, these models typically provide an idealized view of the system. Even when given the same inputs, the model’s behavior can frequently be at variance with some acceptable behavior of the SUT executing on a real platform. We therefore propose steering the model when used as an oracle, to admit an expanded set of behaviors when judging the SUT’s adherence to its requirements. On detecting a behavioral difference, the model is backtracked and then searched for a new state that satisfies certain constraints and minimizes a dissimilarity metric. The goal is to allow non-deterministic, but bounded, behavior differences while preventing future mismatches, by guiding the oracle—within limits—to match the execution of the SUT. Early experimental results show that steering significantly increases SUT-oracle conformance with minimal masking of real faults and, thus, has significant potential for reducing development costs.