Information Technology Reference
In-Depth Information
6.4
Maximal Progress
A property we would like to verify is
maximal progress
. In the context of this
case study, the property can be phrased as: “It is impossible to transfer a single
packet from an input buffer to an output buffer in case a simultaneous packet
transfer is possible.” A modal
μ
-calculus formula that captures this (provided
that it is checked on the model after abstraction of environmental actions) is the
following:
∀
p,q
:
Packet
([
true
](
comm
(0
,
dest
(
p
)
,p
)
|
comm
(1
,
dest
(
q
)
,q
)
true
(5)
⇒
([
comm
(1
,
dest
(
p
)
,p
)]
false
∧
[
comm
(1
,
dest
(
q
)
,q
)]
false
)))
Note that this way of expressing maximal progress does
not
enforce that packet
transfer takes priority over environmental actions.
6.5
Verification Results
The requirements have been checked for the all the (relevant) models, for which
the buffers have capacity 3. This buffer capacity has been chosen because it still
allows for a reasonably fast analysis. The analysis has been conducted with the
mCRL2 tool set (Release 2010, January), on an x86-64 GNU/Linux, running
kernel 2.6.31.12, with an Intel
Core
TM
2 Duo Mobile Processor T9600 and
4GB of RAM.
The results of the formal analysis are captured in Table 1. Requirements
that hold w.r.t. a particular model are marked with “
”.Thetimethatthe
verification took is also indicated. Requirements that are irrelevant for a specific
model are marked with a “-”. It shows that for each of the models all relevant
formulae hold. It should be noted that we have not attempted to reduce these
numbers as much as possible by using state space reduction techniques.
Table 1.
Results of verifying properties on the models
Requirement Simplified Original Modified
1
, 3.550s
, 5m3.863s
, 5m16.921s
, 3.729s
, 7m35.686s
, 7m35.202s
2
3
, 3.778s
, 4m44.647s
, 4m49.101s
4
-
, 5m29.906s
, 5m39.844s
5
, 3.301s
, 4m22.232s
, 4m33.786s
7Comp on
This case study originates form work, gathered in [6]. There, the authors discuss
the same case studies, described in the specification languages: TLA+, Blue-
spec, State-charts and ACP. As we have elaborated on the construction of the
different models with their underlying design decisions in mCRL2, this section
