14. Client/server: test scenario.
Systems with Finite Models 131
0
1
ServerSocket()
13
2
ServerBind()
3
ServerListen()
4
ClientSocket()
5
ClientConnect()
6
ServerAccept()
7
ClientSend()
8
ClientClose()
9
ServerSend(double("99.9"))
10
ServerSend(double("100")) ServerReceive()
12
ServerCloseConnection()
ClientReceive() / double("99.9") ClientReceive() / double("100")
ServerClose()
Figure 7.15. Client/server: test scenario composed with contract model program.
state-dependent parameter generation, or when enabling conditions must depend on
the contract model program state in other ways. Composed programs cannot share
state, so use composition when you can describe the scenario you want in terms
of sequences of actions, without refering to the contract model program state. In
particular, use composition when the scenario can be expressed as an FSM.
7.5 Composition for analysis
We now show how composition can be used for analysis. Recall that the analysis
methods discussed in Chapter 6 require you to write Boolean expressions that
identify unsafe states (for safety analysis) or accepting states (for liveness analysis).
But sometimes it is easier to express requirements in terms of actions, rather than
states. For example, in the reactive system, we can express the safety requirement
132 Structuring Model Programs with Features and Composition
this way: the calibrate action should not follow the arrival of a message containing
an out-of-range temperature.
Pages:
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195