A sequence of actions. A run begins in the initial state and should stop in an
accepting state; otherwise, it is considered a liveness failure.
run-time check. To execute an assertion to check that the program or its environment
is behaving as intended.
safety. The property that nothing bad will happen: execution will not reach any unsafe
states that violate safety requirements. Or, no unsafe scenarios will be executed.
Contrast to liveness.
safety analysis. Checking safety, by searching for unsafe states or attempting to
execute a scenario.
safety requirement. Invariant.
sampling. To limit exploration by selecting desirable paths to explore, rather than
excluding undesirable transitions as with pruning. Sampling is a way to finitize.
Appendices 327
sandbox. A test harness in which normally observable actions are made controllable,
so a normally reactive system can be tested as a closed system.
scenario.Acollection of related runs (perhaps just one).Ascenario can be expressed
by a scenario model program.
scenario control. Limiting analysis and testing to particular runs of interest.
self-loop. A transition where there is no change of state; the current state and next
state are the same. So called because of its appearance in a state transition diagram.
sequence. An ordered collection of (possibly repeating) elements. In the NModel
library, sequence is a compound value.
Pages:
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422