Information Technology Reference
In-Depth Information
Sum.
R
P
=
r
1
+
r
2
,
(
R
P
=
r
1
); (
R
P
=
r
2
) for non-negative
r
1
,
r
2
.
This law expresses that
Time
is dense, as also seen in the derived property:
d
P
e
;
d
P
e,d
P
e
.
Values.
b.
f
=
v
,
(
b.
f
=
v
);
true
and
e.
f
=
v
,
true
;(
e.
f
=
v
).
Induction.
Finite variability of state assertions is crucial for proving invariant
properties. Simple induction over time is not possible, thus it is replaced by
induction over discrete state changes. We do not include the general induction
principle, but its most important consequence, the
P-cover
property
d
P
e
;
true
_d:
P
e
;
true
_ `
=0
with a mirror image
true
;
d
P
e_
true
;
d:
P
e_`
=0
Note that `;' binds stronger than `
_
'and`
^
'.
Standard Form.
In principle, constraints can be formulated using arbitrary
formulas, but a standard form has turned out to be useful because it simplies
reasoning and renement. The basis is a binary operator (
). It expresses that
whenever a
pattern
given by a formula
D
is observed, then it is `followed by' a
goal
state
P
, or stated in a negative form:
−!
de
=
2
D
−! d
P
e
:
(
D
;
d:
P
e
)
This operator behaves like an implication and has a number of distributive laws.
When the pattern says that an assertion holds for an interval, a
Transitive
law
holds:
P
1
e
t
1
−! d
P
2
e
t
2
−! d
P
1
e
t
1
+
t
2
−! d
(
d
P
2
e
)
^
(
d
P
3
e
)
)
(
d
P
2
^
P
3
e
)
This is the law that allows a goal to be achieved through a number of interme-
diate states.
2.3
Requirements Analysis
Requirements are constraints on the behaviours of a system. In order to specify
requirements, application specic
plant states
must be xed. This is illustrated
by the gas burner where the thermostat is modelled by the command state
Heatreq
:
Bool
while controlled states
Flame
;
Gas
;
Ignition
:
Bool
Search WWH ::
Custom Search