Our technology can then
use the model program to automatically generate and check realistic runs of any
desired length. Moreover, our methods can handle nondeterminism, so we can run
more realistic tests where we only control one end of the client/server pair.
We develop a model program for analyzing and testing this system in Chapter 5.
We automatically generate tests from this model program in Chapter 8. Here is a
test run that reveals the defect:
TestResult(0, Verdict("Failure"),
"Action ??™ClientReceive_Finish(double(\"99\"))??™ not enabled in the model",
Unexpected return value of finish action, expected:
ClientReceive_Finish(double "99.9"))
Trace(
Test(0),
ServerSocket(),
ServerBind(),
ServerListen(),
5 For example, see Rainsberger (2005, p. 79).
Overview 31
ClientSocket(),
ClientConnect(),
ServerAccept(),
ServerSend(double("100")),
ClientReceive_Start(),
ClientReceive_Finish(double("100")),
ServerSend(double("99.9")),
ClientReceive_Start(),
ClientReceive_Finish(double("99"))
)
)
The message indicates that this test failed because the value 99 returned by the
client??™s receive method differs from the expected return value 99.9 computed by the
model program. The tool reports the execution of the automatically generated test
run in a syntax that is easy to understand but differs from that of C#. This syntax
expresses the tool??™s internal representation of method calls and returns as data
structures called terms, which provide advantages that we will explain in chapters
to come.
Pages:
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66