In this case all the responses from the server are observable
actions; that is, the actions whose symbol is either ResSetup or ResWork.
16.1.1 Conformance relation
Given is a model program MP and an implementation under test IUT, and the question
under consideration is whether IUT conforms to MP. What does that mean?
There are two ways to answer this question. The first one is declarative; the explanation
is in terms of action traces. The second one is operational; the explanation
is in terms of executing actions in MP and IUT.
Declarative view. The intuition behind this view is what constitutes a failure or a
witness of a conformance violation. MP and IUT do not conform if there exists a
trace of actions that is allowed in both MP and IUT, and after executing that trace
in MP and IUT, either there is a controllable action that is allowed in MP but not
allowed in IUT, or there is an observable action that is allowed in IUT, but not
allowed in MP. In other words, after a sequence of actions which both MP and IUT
agree upon, either there is a controllable action that causes the IUT to throw an
exception, or there is an observable action output by the IUT that causes an enabling
condition violation in MP.
Operational view. The intuition behind this view is how to implement a conformance
tester that detects failures in the above sense. Let SMP stand for the current
state of the MP and let SIUT stand for the current state of the IUT.
Pages:
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343