Information Technology Reference
In-Depth Information
results in a natural meta language due to the use of different semantic models.
With the help from the time modeling language, we can also formulate the
relationship as formulas in DC.
Let
P
be a state variable. Let
P
h
be a state in the sampling time model with
the sampling time step 1
/h
such that
P
h
is interpreted the same as
P
at any
sampling time point, i.e.
(
pt
⇒
P
0
⇔
P
h
0
) (denoted by
samp
(
P, P
h
)),
(
and
(
step
∧
>
0
⇒
(
P
h
∨¬
P
h
)) (denoted by
dig
(
P
h
)). Let
stable
(
P, d
)
denote the formula
((
¬
P
P
¬
P
)
⇒
≥
d
).
Theorem 3.
Let d>
1
/h. The following formulas are valid in DC:
1.
(
stable
(
P, d
)
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
(
P
=
m
⇒|
P
h
−
m
|≤
min
{
,
(
/d
+1)1
/h
}
2.
(
stable
(
P, d
)
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
(
P
=
m
⇒|
P
h
−
∧
dis
)
m
|≤
min
{
,
1
/h/d
}
3.
(
stable
(
P, d
)
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
P
h
=
m
⇒|
P
−
m
|≤
(
/d
+1)1
/h
4.
(
stable
(
P, d
)
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
⇒
P<m
+1
/h
(
/d
+1)
5.
(
stable
(
P, d
)
P
h
<m
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
⇒
P
h
<m
+1
/h
(
/d
+1)
6.
(
stable
(
P, d
)
P<m
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
P
h
>m⇒
P>m−
1
/h
(
/d
+1)
7.
(
stable
(
P, d
)
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
P>m
⇒
P
h
>m
−
1
/h
(
/d
+1)
8.
(
stable
(
P, d
)
∧
samp
(
P, P
h
)
∧
dig
(
P
h
))
⇒
dis
⇒
(
P
h
⇔
P
)
Proof.
This is just a reformulation of Theorem 1 in [9].
This theorem is useful for deriving a valid formula in the original DC from
valid formulas in discrete time model. It can be used in approximate reasoning,
especially in model checking: to check if a system
S
satisfies a DC property
D
,we
can check a sampling system
S
h
of
S
whether it satisfies a discrete DC property
D
h
.
D
h
is found such that
S
h
|
=
D
h
implies
S
|
=
D
. This technique has been
used in [14].
4.2
Periodic Task System
Aperiodictasksystem
T
consists of
n
processes
. Each process
i
raises its request periodically with period
T
i
, and for each period it requests a
constant amount of processor time
C
i
. A specification of system
T
in DC has been
given in many works, see e.g [2], which assume that all the processes raise their
request at time 0. We can give a complete specification of the system without this
assumption using the same technique that was introduced for temporal variable
int
in the previous section. To specify periodic behaviour of process
i
,wealso
{
1
,...,n
}
Search WWH ::
Custom Search