Say MP and IUT
conform from SMP and SIUT if the following two conditions hold:
??? If there is a controllable action a that is allowed in SMP, then a must be allowed
in SIUT , and MP and IUT must conform from the states after executing a.
??? If there is an observable action a that is allowed in SIUT , then a must be allowed
in SMP, and MP and IUT must conform from the states after executing a.
MP and IUT conform, if they conform from the initial states.
Example. Consider the model program SP from Chapter 14 and a server implementation
that may sometimes grant too few credits to the client. In Section 16.3 a mock
implementation of the server is illustrated that has such a bug. Consider the trace in
Advanced Topics 261
Client Server
ReqSetup(0,3)
ResSetup(0,2,Status("Completed"))
ReqWork(1,3)
ReqWork(2,3)
ResWork(1,1,Status("Completed"))
ReqWork(3,3)
ResWork(2,0,Status("Completed"))
ResWork(3,0,Status("Completed"))
Conformance failure!
Figure 16.1. A trace of actions illustrating a conformance failure in SP. Observable actions are sent from
the server to the client.
Figure 16.1. After the first seven actions, the value of window in SP is the empty set
and the only request that is still pending is 3. The implementation then outputs the
response ResWork(3,0,Status("Completed")). This causes a conformance failure,
because this action is not enabled in SP[Credits] (the model program SP with the
Credits feature included).
Pages:
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344