Information Technology Reference
In-Depth Information
for
.Thecases
of relations, propositional connectives and quantication are handled as usual.
For example,
I
and [
b; e
]. The denition is by induction on the structure of
F
=
R
S k
if the duration
R
e
b
I;
[
b; e
]
j
S
I
(
t
)
dt
is at most
k
.For
F
1
;
F
2
(read as
F
1
chop
F
2
) we dene
I;
[
b; e
]
j
=
F
1
;
F
2
if the interval [
b; e
]can
be \chopped" into two subintervals [
b; m
]and[
m; e
]suchthat
I;
[
b; m
]
j
=
F
1
and
I;
F
2
.
Since in our application to the design of real-time systems the initial values
of observables are important, we especially consider time intervals starting at
time 0 and dene that a duration formula
m; e
j
[
]
=
F
holds
in an interpretation
I
i
I;
. To formalise requirements in DC one states a
number of suitable duration formulae and considers all interpretations for which
the conjunction of the DC formulae holds in this sense.
[0
;t
]
j
=
F
for all
t 2
Time
7.2 Semantics of Constraint Diagrams
In this section we indicate how Duration Calculus can be used to provide a
formal semantics for Constraint Diagrams. In fact, we need only a small subset
of Duration Calculus for this semantics. Full details can be found in [12].
Example 3.
Let us consider the CDs for the lter requirements of Section 4 and
use the following abbreviations:
a
abbreviates
in
=
a
for
a 2fno tr; tr; Errorg
A
abbreviates
out
=
A
for
A 2fN; T; Xg
The CD for the
initial state
has the following semantics in Duration Calculus:
de _ dNe
;
true
Thus for every observation interval [0
] the following is required: either it is the
empty interval or it starts with an initial segment where
;t
holds.
In general the semantics of a CD represents an implication of the form
out
=
N
assumptions ) commitments:
Additionally, we use rigid variables
and quantication over them to formulate
common durations in the assumption and commitment part of the implication.
For example, the
lter requirement
has the following semantics:
x
8x; y 2
Time
`
=
x
;(
dtr ^ Ne^`
=
"
); (
dno tr _ tr
)
e^`
=
y^y
5);
true )
`
=
x
+
"
;(
dTe^`
=
y
);
true
Here universal quantication over the rigid variable
represents the unknown
length of the dashed initial part in the corresponding CD. Similarly, the seman-
tics of the requirement
reset after 5 seconds
is represented by the formula
x
8x 2
Time
`
=
x
;(
dTe^`
=5);(
dno tr ^ Ne^`
=
"
);
true )
`
=
x
+5+
"
;
dNe
;
true
Search WWH ::
Custom Search