The methods are based on executable specifications that we call model programs.
To use the methods taught here, you write a model program that represents the
pertinent behaviors of the implementation you wish to specify, analyze, or test. You
write the model program in C#, augmented by a library of data types and custom
attributes. Executing the model program is a simulation of the implementation
(sometimes called an animation). You can perform more thorough analyses by
using a technique called exploration, which achieves the effect of many simulation
runs. Exploration is similar to model checking and can check for safety, liveness,
and other properties. You can visualize the results of exploration as state transition
diagrams. You can use the model program to generate test cases automatically.
When you run the tests, the model can serve as the oracle (standard of correctness)
that automatically checks that the program under test behaved as intended. You can
generate test cases in advance and then run tests later in the usual way. Alternatively,
when you need long-running tests, or you must test a reactive program that responds
to events in its environment, you may do on-the-fly testing, in which the test cases
are generated in response to events as the test run executes. You can use model
composition to build up complex model programs by combining simpler ones, or to
focus exploration and testing on interesting scenarios.
Pages:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25