Information Technology Reference
In-Depth Information
dLine i ( i
n ) which are completely specified by formulas 6, 7 and 8. With
defining HiPri ij in this way, we don't have to assume that all the processes
raise their request at time 0. Hence, reasoning about the correctness of the
scheduler for the general case can be done with the proof system of DC. We
believe that the general model for task scheduling presented in [1] can be clearer
and simplified a lot using this technique.
4.3
Hybrid States and Projection to Discrete Time
In [12], He Jifeng introduced the projection from continuous time to discrete time
to reason about hybrid systems where we have continuous state and temporal
variables. In that paper, intervals are either discrete or continuous. Discrete
intervals are embedded in continuous intervals. He introduced an operator for
projection
\\
defined as: let F and G be a DC formula, then F
\\
G is also a
formula with the following semantics:
I
, [ a, b ]
|
= F
\\
G iff for for some n
N
and
a = m 1
= G ,
where <m 1 ,m 2 ,...,m n > is a discrete interval. In [4], Guelev also showed
that F
m 2
...
m n = b
I
, [ m, m i +1 ]
|
= F and
I
,< m 1 ,m 2 ,...,m n >
|
G can be expressed by a formula in the original DC with a temporal
propositional letter. In the framework of this paper, F
\\
G isdescribedinDC
as follows. We assume two kinds of states in the system: continuous states and
discrete ones. Instead of forcing
\\
to be satisfied by any state, we enforce it to
be satisfied by discrete states only. So, F
SC
\\
G is expressed by
step )
(( F
disemb ( G [ P s /P ]))
where G [ P s /P ] is obtained from G by the substitution of discrete state P s for
state P such that samp ( P, P s ) for each state P occurred in G .Formula(( F
step )
disemb ( G [ P s /P ])) says that the reference interval is discrete interval that
satisfies formula disemb ( G [ P s /P ]), and each discrete step satisfies continuous
formula F . So, with using temporal propositional letters step , the projection
\\
can be defined and reasoning in the original DC as well.
5
Modelling Communication Protocols with Digitizing in
DC
In this section, we show that with discrete time structure formalised, we can
model communication protocols using Duration Calculus (DC) in a very conve-
nient way without any extension for digitising. This model has been presented
in our earlier work [10,7]. Consider a model for communication at the physical
layer (see Fig. 1). A sender and a receiver are connected via a bus. Their clocks
are running at different rates. We refer to the clock of the receiver as the time
reference. The receiver receives signals by digitising. Since the signals sent by
the sender and the signals received by the receiver are functions from the set
+
R
to
(1 represents that the signal is high , and 0 represents that the signal is
low ), we can model them as state variables in DC.
{
0 , 1
}
 
Search WWH ::




Custom Search