Information Technology Reference
In-Depth Information
the properties of time intervals. In this paper, we demonstrate that we can use
this technique to model different time structures and time models. Then, reason-
ing in these time structures can be carried out using the original proof system
of DC and the specification of the structures in DC with continuous semantics.
We show that our technique works well for some case studies.
The paper is organised as follows. In the next section, we give a summary
of Duration Calculus. Our main technique for modelling time structures is de-
scribed in Section 3. Sections 4 demonstrates how our technique can be used for
describing data sampling and projection. In Section 5, we show how the tech-
nique is used in modeling and reasoning in the development of real-time systems
via the well-known case study “Biphase Mark Protocol”.
2
Summary of Duration Calculus
We give a brief summary of Duration Calculus in this section. Readers are re-
ferred to [2] for more details on DC. The version of Duration Calculus we present
here has several additional operators that are useful for the specification pur-
poses.
Time in DC is the set
+
of the non-negative real numbers. For
t, t
∈
R
+
(
t
≤
t
), [
t, t
] denotes the time interval from
t
to
t
.Let
intv
denote the set of all
time intervals.
R
2.1
Syntax of Duration Calculus
Assume that
V
=
{
P,Q,...
}
is a countable set of state variables, and
T
=
is a set of temporal propositional letters. Let
f
n
and
A
n
{
0)
denote
n
-ary function and
n
-ary predicate names respectively. The syntax classes
state expressions
,
terms
,and
formulas
will be then defined as follows.
State expressions:
The set of state expressions is generated by the grammar
X,R,...
}
(
n
≥
S
=0
|
1
|
P
|¬
S
|
S
∧
S,
where
P
stands for state names in the set
V
.
Terms:
The set of terms is generated by
=
S
f
n
(
r,...,r
)
,
r
|
|
where
S
stands for state expressions.
Formulas:
the set of formulas is generated by the grammar:
=
A
n
(
r,...,r
)
D
D
D
|
X
|
|¬
D
|
D
∨
D
|
D
∗
|
0
P
||
P
|
P
where
A
stands for atomic formulas, and
X
for temporal propositional letters.
Search WWH ::
Custom Search