Paul E. Black,
Modeling and Marshaling: Making Tests from Model Checker
19th Digital Avionics Systems
Philadelphia, Pennsylvania (October 2000),
IEEE, section 1.B.3, pages 1-6.
Recently model checkers have been applied to software areas such as
analyzing protocols and algorithms, measuring test adequacy, and
generating abstract tests from formal models. When using model
checkers to generate tests, the generated tests are execution traces
of the models. Thus the type, occurrence, and order of variables,
calls, and events in the execution traces are intimately tied to the
choice of modeling representation.
We briefly review how to use a model checker to generate tests from a
high-level representation, such as MATLAB®, UML, or SCR. Since the
model checker uses a particular general model, the analyst has choices
about how a piece of software may be modeled. We list some choices
and discuss their advantages and disadvantages. We also describe a
program to marshal model variables from resultant model checker traces
and translate them into function calls, program variables, and other
Get the paper in
RTF (93k) or
ASCII text (19k).
This page's URL is /~black/Papers/dasc2000.html
Mon Apr 7 18:21:13 2003
by Paul E. Black
Black's papers or
NIST home page.