Information Technology Reference
In-Depth Information
proc
Input
(
i
:
,c
:
List
(
Packet
)) =
#
c<cap
N
→
enter
(
i, p
)
·
Input
(
i, p
c
)
p
:
Packet
+
c
≈
[]
→
dest
(
p
)
≈
dest
(
rhead
(
c
))
∧
(
¬
int
(
p
)
∨¬
int
(
rhead
(
c
)))
→
p
:
Packet
n
:
N
n
≈
i
→
send
(
i,
dest
(
rhead
(
c
))
,
rhead
(
c
))
|
free
(
n,
dest
(
p
)
,p
)
·
Input
(
i,
rtail
(
c
))
+
c
≈
[]
→
send
(
i,
dest
(
rhead
(
c
))
,
rhead
(
c
))
·
Input
(
i,
rtail
(
c
))
→
n,m
:
N
+
c
≈
[]
grant
(
n, m, p
)
·
Input
(
i, c
)
p
:
Packet
+
c
≈
[]
∧
int
(
rhead
(
c
))
→
dest
(
p
)
≈
dest
(
rhead
(
c
))
→
n
:
N
p
:
Packet
n<i
→
grant
(
n,
dest
(
p
)
,p
)
·
Input
(
i, c
)
+
c
≈
[]
∧
int
(
rhead
(
c
))
→
dest
(
p
)
≈
dest
(
rhead
(
c
))
∧
int
(
p
)
→
n
:
N
p
:
Packet
n>i
→
grant
(
n,
dest
(
p
)
,p
)
·
Input
(
i, c
)
+
c
≈
[]
∧¬
int
(
rhead
(
c
))
→
b
1
(
p
)
≈
b
1
(
rhead
(
c
))
→
n
:
N
p
:
Packet
n<i
→
grant
(
n,
dest
(
rhead
(
c
))
,p
)
·
Input
(
i, c
);
6 Properties of the Models
In [6], the authors presented their models without any form of formal verifica-
tion. For Statecharts this already led to a model that did not meet the design
intent, according to [6]. Their model contained a flaw when both buffers con-
tain interesting head packets and one of the buffers was full while the other was
not. In that case, one packet should be delayed while the other head packet was
routed. This however was not covered.
To convince readers that our models capture the design intent, we formulate
some requirements and verify that the models satisfy them. These requirements
relate to deadlock analysis, overflowing buffers, packet collection and maximum
progress. The requirements are expressed in terms of modal
μ
-calculus formulae.
The mCRL2 tool set allows for checking the validity of such formulae on labelled
transition systems obtained from mCRL2 models.
6.1 Deadlock Detection
Deadlock is a specific condition that brings the system into a halt, from which it
cannot execute any behavior for any future. Deadlock can be caused by various
reasons, amongst others due to circular resource dependencies or when processes
cannot fulfill their precondition in order to execute an extension.
We claim that all of the presented models are free from deadlock. Deadlock
freedom is expressed by the following modal
μ
-calculus formula:
[
true
]
true
true
(1)
