NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Random Testing and Model Checking: Building a Common Framework for Nondeterministic ExplorationTwo popular forms of dynamic analysis, random testing and explicit-state software model checking, are perhaps best viewed as search strategies for exploring the state spaces introduced by nondeterminism in program inputs. We present an approach that enables this nondeterminism to be expressed in the SPIN model checker's PROMELA language, and then lets users generate either model checkers or random testers from a single harness for a tested C program. Our approach makes it easy to compare model checking and random testing for models with precisely the same input ranges and probabilities and allows us to mix random testing with model checking's exhaustive exploration of non-determinism. The PROMELA language, as intended in its design, serves as a convenient notation for expressing nondeterminism and mixing random choices with nondeterministic choices. We present and discuss a comparison of random testing and model checking. The results derive from using our framework to test a C program with an effectively infinite state space, a module in JPL's next Mars rover mission. More generally, we show how the ability of the SPIN model checker to call C code can be used to extend SPIN's features, and hope to inspire others to use the same methods to implement dynamic analyses that can make use of efficient state storage, matching, and backtracking.
Document ID
20150014750
Acquisition Source
Jet Propulsion Laboratory
Document Type
Conference Paper
External Source(s)
Authors
Groce, Alex
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Joshi, Rajeev
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
August 3, 2015
Publication Date
July 20, 2008
Subject Category
Mathematical And Computer Sciences (General)
Meeting Information
Meeting: ACM Workshop on Dynamic Analysis
Location: Seattle, WA
Country: United States
Start Date: July 20, 2008
End Date: July 24, 2008
Sponsors: Association for Computing Machinery
Distribution Limits
Public
Copyright
Other
Keywords
dynamic analysis

Available Downloads

There are no available downloads for this record.
No Preview Available