8: a sandbox where both the client
and server are controlled by the test runner, and both execute in a single thread,
interleaving their method calls in an order that conforms to their protocol (Chapter 2,
Figure 2.2).
We want a contract model that can generate all the runs that the client and server
can successfully execute in the sandbox. By a ???run,??? we mean a session where both
client and server create sockets, possibly exchange some messages, and then close
their sockets. By ???successfully execute,??? we mean every method call returns, and no
Systems with Finite Models 73
exceptions are thrown. Therefore, certain sequences of method calls are forbidden.
If the client attempts to connect before the server is listening on its socket, the client
throws an exception. If one partner attempts to receive before the other partner
sends, the receive method will block and never return. The model program must not
generate runs like these.
The runs that the implementation can execute depend on its configuration. If
the client and server run in separate threads, then one partner could call its receive
method before the other partner sends. A different model program would be needed
to model that configuration. Selecting the configuration can be an important step in
preliminary analysis.
The challenges in this example are to write a model program that generates all
the runs we want but none that are forbidden, and that generates enough different
temperatures to expose the defect while keeping the model finite.
Pages:
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119