Generating MC/DC Adequate Test Sequences Through Model Checking

S
SEW
2003
28th Annual NASA Goddard Software Engineering Workshop (SEW'03)
Abstract - Generating MC/DC Adequate Test Sequences Through Model Checking

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Sanjai Rayadurgam Articles by Mats P. E. Heimdahl

28th Annual NASA Goddard Software Engineering Workshop (SEW'03)

Greenbelt, Maryland

December 03-December 04

ISBN: 0-7695-2064-2

	ASCII Text	x
	Sanjai Rayadurgam, Mats P. E. Heimdahl, "Generating MC/DC Adequate Test Sequences Through Model Checking," Software Engineering Workshop, Annual IEEE/NASA Goddard, pp. 91, 28th Annual NASA Goddard Software Engineering Workshop (SEW'03), 2003.

	BibTex	x
	@article{ 10.1109/SEW.2003.1270730, author = {Sanjai Rayadurgam and Mats P. E. Heimdahl}, title = {Generating MC/DC Adequate Test Sequences Through Model Checking}, journal ={Software Engineering Workshop, Annual IEEE/NASA Goddard}, volume = {0}, year = {2003}, isbn = {0-7695-2064-2}, pages = {91}, doi = {http://doi.ieeecomputersociety.org/10.1109/SEW.2003.1270730}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Software Engineering Workshop, Annual IEEE/NASA Goddard TI - Generating MC/DC Adequate Test Sequences Through Model Checking SN - 0-7695-2064-2 SP EP A1 - Sanjai Rayadurgam, A1 - Mats P. E. Heimdahl, PY - 2003 KW - null VL - 0 JA - Software Engineering Workshop, Annual IEEE/NASA Goddard ER -

Sanjai Rayadurgam, University of Minnesota, Minneapolis

Mats P. E. Heimdahl, University of Minnesota, Minneapolis

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEW.2003.1270730

We present a method for automatically generating test sequences to satisfy MC/DC likes structural coverage criteria of software behavioral models specified in state-based formalisms. The use of temporal logic for characterizing test criteria and the application of model-checking techniques for generating test sequences to those criteria have been of interest in software verification research for some time. Nevertheless, criteria for which constraints span more than one test sequence, such as the Modified Condition/Decision Coverage (MC/DC) mandated for critical avionics software, cannot be characterized in terms of a single temporal property.

This paper discusses a method for recasting two-sequence constraints in the original model as a single sequence constraint expressed in temporal logic on a slightly modified model. The test-sequence generated by a model-checkder for the modified model can be easily separated into two different test-sequences for the original model, satisfying the given test criteria. The approach has been successful in generating MC/DC test sequences from a model of the mode-logic in a flight-guidance system.

Citation:

Sanjai Rayadurgam, Mats P. E. Heimdahl, "Generating MC/DC Adequate Test Sequences Through Model Checking," sew, pp.91, 28th Annual NASA Goddard Software Engineering Workshop (SEW'03), 2003

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.