Information Technology Reference
In-Depth Information
express the physical state of the flame, gas and ignition.
A particular requirement is typically a
commitment
that the design shall
satisfy under certain
assumptions
about the plant. Assumptions are essentially
properties which we during the design assume satised by the plant. In other
words, they are commitments in the design of the plant as such with the role of
command and controlled states reversed. Thus, we can reasonably expect that
commitments and assumptions express similar properties which typically are
specied by the following kinds of formulas.
Progress.
The rst kind species
progress properties
: When the command or
the controlled states satisfy an assertion
P
, the controlled states will move to a
region specied by an assertion
Q
within a given time
t
.
e
t
−! d
d
P
Q
e
These commitments are analogous to concrete stability requirements for a mode
of operation that is given by
P
. It is easy to see that the commitments
O
(
60
60
d:
Heatreq
e
−! d :
Flame
e
)and
On
(
d
Heatreq
e
−! d
Flame
e
)forthe
burner are of this form.
In fact, also the assumptions for
On
can be given this form, e.g.,
:
FlameFail
1
is
.
A progress commitment allows a design to ignore unstable modes. If
P
is
oscillating with a period shorter than
t
(An example could be the thermostat
going on and o with a period shorter than 60,) the formula is trivially true, and
the design may focus on other commitments. This is in contrast to the
bounded
progress
property of [4] which states that occurrence of
P
leads to
Q
within
t
,
or
d
Gas
^
Flame
e−!d
Flame
e
,and
:
IgniteFail
is
d
Gas
^
Ignition
e
−! d
Flame
e
(
d
P
e
;(
`
=
t
)
)
d
Q
e
)
This formula requires a design to react on any occurrence of
P
. Any practical
design must therefore at some point assume some minimal period, or alterna-
tively weaken the commitment to express that an unstable mode is ignored:
(
d
P
e
;(
`
=
t
)
)
d:
P
_
Q
e
). A formula that is equivalent to
e
t
)
(
d
P
d
Q
e
)
This looks like a very reasonable formulation of progress. However, it is inconve-
nient when the commitment says that the system should leave a mode
P
within
time
t
, because taking
Q
to be
:
P
in the formula above gives a contradiction,
e
t
−! d :
while
d
P
P
e
expresses exactly the desired property within the progress
framework.
Bounded Invariance.
A progress constraint ensures that a system will move
towards a goal when the current state is stable. The constraint is trivial if the
current state is unstable. At the top level of requirements it is very useful to
Search WWH ::
Custom Search