Lockstep execution is supported by
a test harness called a stepper.
loop extension. In composition, the model program formed by adding actions that
are self-loops for each of the actions in the other model programs that are not shared
actions.
map. A collection that associates unique keys with values. In the NModel library,
map is a compound value.
match. Determining which actions in separate model programs will be combined
in composition. Matching considers both action symbols and argument values.
memoryless. A strategy that does not remember the history of previous action
selections. Contrast to adaptive.
324 Glossary
model checking. An analysis technique similar to exploration that usually checks a
property expressed as a formula in temporal logic.
model program.Aprogram that describes the behavior of another program, system,
or component called the implementation. A model program can act as a specification
or a design.We distinguish contract model programs from scenario model programs.
model-based analysis. Using a model program to debug and improve specifications
and designs. Simuluation, exploration, and composition are model-based analysis
techniques. They can be used for safety analysis or liveness analysis.
model-based testing. Using a model program to generate test cases or act as an
oracle. Model-based testing includes both offline testing and on-the-fly testing.
Pages:
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417