Information Technology Reference
In-Depth Information
have such under-determined constraints. They absorb gracefully all questions
about the behaviour of the system under unstable command inputs, because
they allow any implementation. However, when components are designed or when
stating assumptions, it is useful to give additional constraints that ensure orderly
progress by limiting the selection of goal states.
When a progress constraint
e
t
−! d
d
P
Q
e
is implemented by some atomic
d
e−!d
_
e
transition, it satises an invariant
, i.e., when
P
is entered, it is
stable until left for
Q
. Due to progress, it must be left at the latest after
t
time
units. If we want to express that this invariance is time-bounded by
t
,wemust
identify the start of the
P
phase in the pattern:
P
P
Q
(
d:
P
e
;
d
P
e^`
t
)
−! d
P
_
Q
e
This formula states that a current state
P
for a period of
t
time units will either
remain stable or transit to
Q
.
A special case of invariance keeps a current state stable. This is important
in communication, because it gives other systems time to observe the current
state. Unbounded invariance of
P
is
. If the system ever enters state
P
, then it will stay there for ever on. More useful is bounded invariance, where
a system stays in
P
for some xed period
t
:
d
P
e−!d
P
e
(
d:
P
e
;
d
P
e^`
t
)
−! d
P
e
Such an invariance ensures stability of
P
, as expressed in the following law,
(
d:
P
e
;
d
P
e^`
t
)
−! d
P
e,
(
d:
P
e
;
d
P
e
;
d:
P
e)`>
t
)
In order to illustrate the flavour of a proof in duration calculus, we prove the
implies part by contradiction.
d:
P
e
;
d
P
e
;
d:
P
e^`
t
)f
Sum
g
(
d:
P
e
;
d
P
e
;
d:
P
e^`
t
);
d:
P
e)f
Assumption
g
false
The proof uses that the negation of
2
(
d:
P
e
;
d
P
e
;
d:
P
e)`>
t
) is the formula
t
). Using monotonicity of chop, we will have disproved
this formula if we disprove the initial formula. The second step uses the Sum
law to chop the last subinterval where
(
d:
P
e
;
d
P
e
;
d:
P
e^`
P
holds and to deduce that the length
of subintervals is not greater than the length of the initial interval. The third
step uses the assumption (
:
d:
P
e
;
d
P
e^`
t
)
−! d
P
e
which by denition is
) which directly gives the contradiction.
Bounded invariance commitments are strong constraints that remove much
non-determinism and thus design options. They should not be introduced with-
out some consideration of the intended implementation technology. In a design,
they can be rened to formulas of the same form and involving the same states,
but ultimately they depend on assumption of some atomic invariance, analo-
gous to Lipschitz conditions in a continuous model. It will thus assist a designer,
if bounded invariance constraints are replaced by the weaker critical duration
constraints, discussed in a following.
:
((
d:
P
e
;
d
P
e^`
t
);
d:
P
e
Search WWH ::
Custom Search