One common case is when one of the model programs represents the model of the
expected behavior, whereas the other model programs are various scenarios.
Probes. In some applications of model-based testing, it is useful to be able to check
that some abstract view of the state of the IUT is consistent with the corresponding
view of the model state. The actions that provide or check that view are sometimes
called probes (or observers). The main property of a probe is that it does not change
the state, that is, that the resulting state transition is a self-loop.
Let us consider a concrete example using the bag model. First, we add a new
feature called Probe to the bag model that contains a new action symbol CheckView.
The purpose of a CheckView action is to serve as a probe. An action CheckView(v)
that is enabled in a state s provides an abstract view of s by showing that the set
of elements in the bag is v. The view is clearly an abstraction of the actual state
because the multiplicity of the individual elements is omitted.
namespace BagModel
{
[Feature]
static class Probe
{
static Set
> E()
{ return new Set>(Contract.content.Keys); }
[Action]
static void CheckView([Domain("E")]Set elems) { }
static bool CheckViewEnabled(Set elems)
{ return elems.Equals(Contract.content.Keys); }
}
}
Test harness. When new actions, such as CheckView, are added to the model program,
the test harness may need some adaptation.
Pages:
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285