Information Technology Reference
In-Depth Information
If
D
=
D
(
ρ
)
<
1, then
•
¬
Y
∧
int
∧
≥
g
(
D
LHR
(
=
d
)
(
ρ
)
<
1) =
g
(
D
)0 , and
Y
∧
int
∧
≥
g
(
D
LHR
(
=
d
)
(
ρ
)
<
1) =
g
(
D
)1.
¬
Y
∧
int
∧
≥
>
0)
(
int
1)
LHR
(
=
d
)
LHR
(
=
For example, let
D
be (
≤
1
∧
∧
=
r
−
d
)
HLR
(
=
d
)
(
int
)
(
<
1)). Then,
Y
∧
>ρ
∧
g
(
D
)=
g
((
≤
1
∧
>
0)
(
int
∧
=
r
−
1)
LHR
(
=
d
)
LHR
(
=
d
)
(
Y
∧
>ρ
∧
int
)
(
<
1)) 1
=
g
((
≤
1
∧
>
0)
(
int
∧
=
r
−
1)
LHR
(
=
d
)
int
)
(
<
1)) 01
(
¬
Y
∧
>ρ
∧
>
0)
(
int
=
g
((
≤
1
∧
∧
=
r
−
1)
(
int
)
(
<
1)) 101
¬
Y
∧
>ρ
∧
=
101
.
5.2
Verification of BMP
As said earlier, we have to verify that for any sequence of bits
w
, if the sender
puts on the bus the signal represented by DC formula
f
(
w
), then the receiver
must receive and receives only the signals represented by a DC formula
D
for
which
g
(
D
)=
w
. We can only prove this requirement with some condition on
the values of the parameter
r, a, b, c, ρ
and
d
. The requirement is formalised as:
For all sequence of bits
w
,
-
there exists a DC formula
D
received by the receiver such that
f
(
w
)
⇒
D
,
and
-
for all
D
receivable by the receiver, if
f
(
w
)
⇒
D
then
g
(
D
)=
w
.
Since in BMP
g
is a deterministic function, for any sequence of bits
w
there is
no more than one receivable formula
D
for which
f
(
w
)
⇒
D
.Thuswecanhave
a stronger requirement which is formalised as:
For all sequences of bits
w
there exists uniquely a receivable formula
D
such
that
f
(
w
)
D
and
g
(
D
)=
w
.
Our verification is done by proving the following two theorems.
⇒
Theorem 4.
For any receivable formulas D and D
,ifD is different from D
syntactically then
D
)
|
=((
D
∧
⇒
ff
)
.
This theorem says that each time at most one receivable formula
D
is received
by the receiver.
Theorem 5.
Assume that r
≥
1
, b
≥
r
+1
, a
≥
r
+1
, c
≥
ρ
+
a, d
≥
b
+
r,
d
a
+1
. Then for any sequence of bits w there exists a
receivable formula D for which f
(
w
)
≤
a
+
b
−
3
−
r,andρ
≥
⇒
D and g
(
D
)=
w.
In [7] we proved these two theorems, with PVS proof checker, with the encoding
of the proof system for Duration Calculus.
Search WWH ::
Custom Search