Skip to main content
U.S. flag

An official website of the United States government

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.

Testing with Model Checkers: Insuring Fault Visibility

Published

Author(s)

Vadim Okun, Paul E. Black, Y 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.
Conference Dates
October 21-23, 2002
Conference Location
Rio de Janeiro
Conference Title
2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems

Keywords

fault-based testing, formal methods, model checking, mutation checking, mutation testing, SMV, software engineering, specification-based testing, state machine

Citation

Okun, V. , Black, P. and Yesha, Y. (2002), Testing with Model Checkers: Insuring Fault Visibility, 2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems, Rio de Janeiro, -1, [online], https://tsapps.nist.gov/publication/get_pdf.cfm?pub_id=50790 (Accessed March 28, 2024)
Created October 23, 2002, Updated February 19, 2017