Testing with Model Checker: Insuring Fault Visibility

Vadim Okun; Paul E. Black; Yelena Yesha

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

PUBLICATIONS

Testing with Model Checker: Insuring Fault Visibility

Published

January 5, 2003

Author(s)

Vadim Okun, Paul E. Black, Yelena Yesha

Abstract

To detect a fault in software, a test case execution must be chosen so intermediate errors propagate to the output. We describe two modeling methods for specification-based mutation testing using model checkers that guarantee this propagation. We evaluate the methods empirically and show that they yield more useful tests than the previous "direct reflection" methods.

Citation

WSEAS Transactions on Systems

Volume

Issue

Pub Type

Journals

Download Paper

Local Download

Keywords

formal methods, model checking, specification-based testing, mutation testing

Software testing

Citation

Okun, V. , Black, P. and Yesha, Y. (2003), Testing with Model Checker: Insuring Fault Visibility, WSEAS Transactions on Systems, [online], https://tsapps.nist.gov/publication/get_pdf.cfm?pub_id=917181 (Accessed April 27, 2026)

Additional citation formats

Issues

If you have any questions about this publication or are having problems accessing it, please contact [email protected].

Created January 5, 2003, Updated February 19, 2017

Was this page helpful?