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{infusion
author = {Anitha Murugesan, Gregory Gay, Sanjai Rayadurgam, Mats Heimdahl },
title = {Infusion Mgr Model and Testing Data},
howpublished= {\url{http://crisys.cs.umn.edu/PublicDatasets.shtml}}

@inproceedings{Gay:2014:IAO:2642937.2642989,
 author = {Gay, Gregory and Rayadurgam, Sanjai and Heimdahl, Mats P.E.},
 title = {Improving the Accuracy of Oracle Verdicts Through Automated Model Steering},
 booktitle = {Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering},
 series = {ASE '14},
 year = {2014},
 isbn = {978-1-4503-3013-8},
 location = {Vasteras, Sweden},
 pages = {527--538},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2642937.2642989},
 doi = {10.1145/2642937.2642989},
 acmid = {2642989},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {model-based testing, software testing, test oracles},
}

About the Data

Overview of Data

Infusion pumps are medical cyber physical systems used for controlled delivery of liquid drugs into a patient’s body according to a physician’s prescription (the set of instructions that governs infusion rates for a medication). These pumps may be classified into various kinds depending on their features, construction, and usage. Patient-Controlled Analgesia (PCA) pumps are generally equipped with a feature that allows patients to self-administer a controlled amount of drug (a patient-bolus), typically a pain medication.

In an infusion system, the clinician operates the GPCA device, programs the prescription information, loads the drug, connects the device with the patient, and responds to exceptional conditions that occur during the therapy. The patient receives the medication from the device through an intravenous needle. The patient can self-administer prescribed amounts of additional drug by requesting a bolus, a request usually done by pressing a bolus request button accessible at the patient’s bed. The hospital pharmacy database is a repository that stores manufacturer provided drug information (for example, upper limits on infusion rates for a specific drug).

In short, the GPCA system has three primary functions: (1) deliver the drug based on the prescribed schedule and patient requests, (2) prevent hazards that may arise during its usage, and (3) monitor and notify the clinician of any exceptional conditions encountered.

This package contains a model of the prescription management behavior of the software of an infusion pump, a version of the model with read faults, a set of seeded mutants, and associated test inputs used for model-based testing research.

For more information on this model, please see: Anitha Murugesan, Michael Whalen, Sanjai Rayadurgam and Mats Heimdahl. Compositional Verification of a Medical Device System. Accepted at High Integrity Language Technology Accepted at High Integrity Language Technology, Pittsburg, Nov 2013

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 - 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.

Data Categories

Infusion Manager

URL