Information Technology Reference
In-Depth Information
6.2
Absence of Overflowing Buffers
We have used the standard mCRL2 type construction of lists for modeling the
contents of the buffer. Thought the lengths of such lists are not fixed or bound
from above, the use in combination with the constant
cap
guarantees that there
can be no overflows of the buffers. By means of adding the alternative summand:
#
c
>
cap
→
overflow
·
Input
(
i, c
)
to the input buffers, and the summand
#
c
>
cap
→
overflow
·
Output
(
i, c
)
to the output buffers, we can easily check that this situation can never occur by
verifying the validity of the modal formula
[
true
·
overflow
]
false
(2)
on the model that is obtained after abstracting from all actions besides
overflow
.
This formula then expresses that there can be no execution that performs the
action
overflow
.
6.3
Absence of Colliding Packets
The property that no simultaneous packet transfers are possible to the same
output buffer is specified by means of the following modal
μ
-calculus formula:
∀
p,q
:
Packet
∀
i,j,k
:
N
[
true
∗
.
(
comm
(
i, j, p
)
|
comm
(
k, j, q
))]
false
(3)
This formula must be checked on the model after abstraction from all other
actions. This means that for the Simplified Switch the following model has been
used
init
τ
{enter,leave}
(
∂
{send,recv ,grant,free}
(
Γ
{send|recv |grant→comm}
(
Γ
{send|recv |free→comm}
(
Input
(0
,
[])
Input
(1
,
[])
Output
(0
,
[])
Output
(1
,
[])))));
In a similar way, abstract models for Original and Modified Switch can be
defined.
It is not allowed to send two interesting packets simultaneously. This is verified
by checking the modal
μ
-calculus formula
[
true
.
(
comm
(
i, j, p
)
∀
p,q
:
Packet
∀
i,j,k,l
:
N
(
int
(
p
)
∧
int
(
q
))
⇒
|
comm
(
k, l, q
))]
false
(4)
on the system where all environmental actions are abstracted from.
Requirement 3 is relevant for all three models discussed in this paper and
Requirement 4 is only relevant for the latter two models.
