In Chapter 7 we will discuss another kind of analysis. Instead of searching for
unsafe states or dead states, that analysis checks temporal properties defined by
sequences of actions.
114 Exploring and Analyzing Finite Model Programs
6.4 Exercise
1. Explore a program with mpv, with MaxTransitions set low enough so that the
FSMis not completely explored. Try several different values for MaxTransitions.
Does it appear that mpv explores the FSM depth-first, breadth-first, or in some
other way?
7 Structuring Model
Programs with
Features and
Composition
In this chapter we describe two mechanisms for structuring model programs at
a large scale: features and composition. Each provides a way to combine model
programs in order to create a new one, or to write a model program as a collection
of parts that are themselves complete (or nearly complete) model programs.
Both mechanisms are so versatile that they can be used in many ways. In Chapter
14 we use them to model interacting features. In this chapter we use them to
limit analysis and testing to particular scenarios of interest.We also show how composition
can be used in analysis to check temporal properties defined by sequences
of actions.
7.1 Scenario control
The problem of limiting analysis and testing to particular runs of interest is called
scenario control. Scenario control is necessary because we usually write a model
program to act as a specification or contract, so it describes everything the implementation
must do, might do, and must not do.
Pages:
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175