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.

Abstracting Formal Specifications to Generate Software Tests via Model Checking

Published

Author(s)

P E. Ammann, Paul E. Black

Abstract

A recent method combines model checkers with specification-based mutation analysis to generate test cases from formal software specifications. However high-level software specifications usually must be reduced to make analysis with a model checker feasible.We propose a new reduction, parts of which can be applied mechanically, to soundly reduce some large, even infinite, state machines to manageable pieces. Our work differs from other work in that we use the reduction for generating test sets as opposed to the typical goal of analyzing for properties. Consequently, we have different criteria, and we prove a different soundness rule. Informally the rule is that counterexamples from the model checker are test cases for the original specification. The reduction changes the state machine and temporal logic constraints in the model checking specification to avoid generating unsound test cases. We give an example of the reduction and test generation.
Citation
Digital Avionics Systems Conference

Keywords

abstraction, formal methods, model checking, reduction, software, software quality, test generation, testing

Citation

Ammann, P. and Black, P. (1999), Abstracting Formal Specifications to Generate Software Tests via Model Checking, Digital Avionics Systems Conference, [online], https://tsapps.nist.gov/publication/get_pdf.cfm?pub_id=151677 (Accessed February 25, 2024)
Created September 30, 1999, Updated October 12, 2021