Information Technology Reference
In-Depth Information
Regarding Statecharts, the authors of [6] did not give a suitable description
in their paper, as they specified a wrong model. Therefore a comparison for
maximal throughput, renders useless as a throughput analysis on Statecharts is
omitted. Note that this does not mean that it is impossible to give a correct
model using Statecharts.
7.2
Priority
The locality of reasoning is derived from the way priority is assigned to the
routing of packets.
To reduce the amount of global reason, w.r.t. the communication we have
generalized from the specific implementations of the input buffers. This allows
us to reason on a local level about priorities. This shows if we compare our
models to those as given in ACP. Note that within mCRL2, we have modelled
priority by means of permissions, and therefore the contents of the buffers are
invisible to other processes. In the given ACP models, the queues are directly
inspected by the other processes. This requires a more spatial reasoning in ACP,
in order to derive the priority.
Within TLA+, the priority of a packet transfer is handled at a local level. So
with respect to assigning priority to executing actions, mCRL2 and TLA+ are
comparable. We do have to note that the input queues, as well as the output
queues are grouped in TLA+. This makes it possible for TLA+ actions to directly
observe the queue of another process, at a local level. When comparing this
method to the one given in our models, we believe that it is possible in mCRL2
to apply reasoning on a more local level.
The Bluespec specification defines rules that implicitly deal with mutually
exclusive access to shared resources. When multiple rules access the same re-
source, access is given to the resource defined first in the priority hierarchy. In
this way, priority amongst packet transfers is ensured. Note that priority rules
are defined on a spatial level. Therefore, the reasoning that needs to be applied
is more spatial than the one used in mCRL2.
Within Statecharts all the behavior of the buffers are locally specified, however
global temporal reasoning is required to establish the priority among packet
transfers. A simultaneous transfer requires a global spatial reasoning over at
least four individual Statecharts.
7.3
Adaptability
In [6], the authors only explain TLA+ for the simple switch. Though they claim
that TLA+ relates to Bluespec, they do not show models for the original and
modified switch. For that reason, the adaptability of TLA+ is unclear, since we
are no experts in it. This does not permit us to judge whether mCRL2 performs
better or worse in terms of adaptability.
A similar reasoning holds for Statecharts. The authors describe in a fairly
easy way how to obtain a simple switch from the original switch. However,
the subsequent discussion they show that the presented model of the original
