Information Technology Reference
In-Depth Information
calculus. The logical foundations of duration calculus are treated thoroughly in
[3], while other selected applications are found in [7, 9, 12, 13, 10].
The basis for duration calculus is a dynamical systems model with state
functions that for each point of real time assign a value to the
states
.Inthecase
of the gas burner
Heatreq
;
Flame
;
Gas
;
Ignition
:
Bool
express the physical state of the thermostat, the flame, the gas supply, and the
ignition transformer. The requirements are then given by the invariance of the
following formulas over arbitrary, closed intervals of time [
b
;
e
]with
b
;
e
denoting
non-negative real numbers, satisfying
b
e
.
Safe.
For Safety, gas must never leak for more than 4 seconds in any period of
at most 30 seconds
)
R
(
Gas
`
30
^:
Flame
)
4
In this formula, the interval function
`
is the
length
of the interval (
e
−
b
), and
the
duration
term
R
(
Gas
^:
Flame
) is the integral over the interval of the state
expression
Gas
Flame
. It denotes exactly the (accumulated) duration of the
unsafe state when gas is leaking.
^:
O.
Heat request o shall result in the flame being o after 60 seconds
d:
e)`
_
`
d:
e
Heatreq
60
((
= 60);
Flame
)
The premise in this formula asserts that the state
:
Heatreq
essentially holds for
de
=(
R
the full interval:
d:
Heatreq
e
:
Heatreq
=
`
)
^
(
`>
0). In this sub-formula,
the conjunct
0 ensures that it is a proper interval, and not a point where
b
=
e
. The conclusion (
`>
asserts that the interval can be
\chopped" (the `;' operator) into subintervals [
b
`
= 60);
d:
Flame
e
;
m
]and[
m
;
e
] such that
`
=60
holds for [
b
;
m
]and
d:
Flame
e
for [
m
;
e
].
On.
Heat request shall after 60 seconds result in gas burning unless an ignite
or flame failure has occurred
d
Heatreq
e)`
60
_
((
`
= 60);
d
Flame
e
)
_
(
IgniteFail
_
FlameFail
)
_
The exceptional conditions are specied by
3
(
IgniteFail
FlameFail
) which
asserts that somewhere in the interval an
IgniteFail
or an
FlameFail
occur.
For the moment we leave the formulas denoted by
IgniteFail
and
FlameFail
unspecied.
It is clear that the requirements
On
and
O
are bounded progress properties;
they require that a certain state is reached within a given time. Such properties
are analogous to stability of a dynamical system: after some time the system
remains in some bounded region. It is also intuitively clear that in programming
Search WWH ::
Custom Search