2):
ct /r:Stepper.dll /iut:ClientServerImpl.Stepper.Create ?†
/testSuite:ScenarioTest.txt
3 A complete command reference for ct appears in Appendix B.3.
Systems with Finite Models 147
When we execute this command, the test fails:
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(),
ClientSocket(),
ClientConnect(),
ServerAccept(),
ServerSend(double("100")),
ClientReceive_Start(),
ClientReceive_Finish(double("100")),
ServerSend(double("99.9")),
ClientReceive_Start(),
ClientReceive_Finish(double("99"))
)
)
The output shows the trace of the actual test run through the action that failed
(compare to the trace of the test case in Figure 8.3). The message indicates that this
test failed because the return value 99 in the last finish action is not the same as the
expected return value 99.9 computed by the model program and stored in test case.
8.5 Limitations of offline testing
The five test cases in the first test suite all pass; they do not reveal the defect in
the implementation that we discussed in Chapter 2, Section 2.10. Recall that the
defect causes a failure after the server sends the client more than four characters
(e.g., "100.
Pages:
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215