Information Technology Reference
In-Depth Information
switch is incorrect and requires a more complicated model to capture the design
intent. Since this correct complicated model is not given, it is not fair to make
a comparison.
For modeling the modified switch in Bluespec, the authors require an entire
redesign of the original switch, such that each priority separately defines rules.
This leads to almost a duplication of the model. As we compare the same exten-
sion for our modified switch in mCRL2, we only have to split a summand and
alter a guard, which is a rather small modification.
ACP serves well in terms of adaptability for this case study. As mCRL2 falls
in the same category as ACP, this also holds for mCRL2. Therefore in terms of
adaptability, mCRL2 and ACP are comparable.
Furthermore, we have set up the processes of the buffers in such a way that
they can be easily reused for a more general specification, e.g. a
N
M
specifi-
cation. To do so, we are required to add extra process references in the initial-
isation, and add extra rules to the data equations for routing packets. Within
the current models we allow, that only one packet can be send simultaneously
within a clock cycle. By adding more processes, this bound will not change. To
increase the throughput, e.g. allowing more message transfers per clock cycle,
we need to add summands that grant this communication. We argue that these
modifications can be done at a local level.
×
7.4
Verification
The authors of [6] are unable to convince themselves that the specification they
give are correct with respect to the design intent. As their remark essentially
holds for all specifications, it already shows the first pitfalls in concurrent system
design.
In line with the authors of [6], we agree that global reasoning is required
on a specification across all the processes to verify system requirements. This
however is a dicult task. As the description of the models is fairly simple,
their explicit behaviour is not. In Figure 1 we have taken the opportunity to
show, that even for a small system like the simplified switch, it already leads to
systems that cannot be overlooked by human reasoning
1
. For a buffer capacity of
three elements, we generate a state-space of 3600 states with 41137 transitions
2
.
Nevertheless, with the automated methods of the mCRL2 tool set it turns out
to be possible to verify interesting properties of the modelled systems. This does
not require reasoning by humans, which is the case for establishing properties
using the formalisms used in [6].
1
These numbers are obtained, without applying any reduction techniques. We are
aware that these numbers can be reduced. Note that the number of states and the
number of transitions are given on a logarithmic scale.
2
Please note that multi-actions that contain precisely the same actions are only taken
into account once. Otherwise, the numbers of transitions would have been much
larger.
