We write
a model program in order to answer some questions about the implementation (by
testing or analysis).We have to formulate those questions before we can see how to
write the model program.
In this example, our questions arise from the observation that the newsreader
presents several kinds of pages that can be formatted in various styles, and several
options for selecting pages and styles. Our questions are: What options are available
when a particular page and style is displayed? What page and style appears when
the user selects a particular option?
Our questions guide testing and analysis. To create a test suite, we express the
questions this way: Are the intended options made available for each particular page
and style? Does the intended page and style appear when each particular option is
chosen? To perform liveness analysis, we ask: Is every option available (on some
page)? Can every page and style be made to appear (by choosing some sequence of
options)? Are there are any deadlocks (pages with no options) or livelocks (pages
from which other pages cannot be reached)? To perform safety analysis, we ask:
Are the options that are available on each page the ones that should be there? Is it
possible to request some combination of page and style that doesn??™t make sense?
5.3.2 Select the features
We usually do not model a large system with a single model program.
Pages:
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102