In the NModel framework, model programs are written in C#, augmented by a
library of attributes and data types. Methods in the model program represent the
actions (units of behavior) of the implementation. Variables in the model program
represent the state (stored information) of the implementation. Each distinct combination
of values for the variables in the model program represents a particular state
(situation or condition) of the implementation.
Within a model program, we can identify separate features (groups of related
variables and methods).We can then perform analysis or testing limited to particular
features or combinations of features.
We can write separate model programs and then combine them using composition.
Composition is a program-transformation technique that is performed automatically
by our analysis and testing tools, which can then analyze or test from the
composed program. Composition is defined (and implemented by the tools) in a
way that makes it convenient to specify interacting features, or to limit analysis and
testing to particular scenarios, or to describe temporal properties to check during
analysis.
Overview 5
To see how to write a model program, we can refer to traditional, informal speci-
fications and design documents. Sometimes there is already an implementation we
can inspect or experiment with. Sometimes a designer will write the model program
first, going directly from ideas to code.
Pages:
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29