Information Technology Reference
In-Depth Information
describes the deviation of the formalisms with respect to the case study. The
comparison focusses on three aspects, namely locality of reasoning, adaptability
of the language and maximal throughput. Furthermore we extend the focus by
taking verification into account.
Before explaining the comparison, we give a brief description of the four lan-
guages. First, TLA+ (the Temporal Logic of Actions) is a complete specifica-
tion language, that uses logic for the specification and reasoning about concur-
rent and reactive systems. It is designed for writing specifications consisting of
non-temporal mathematics with temporal logic and tries to capture a complete
system in a single formula [14]. Second, Bluespec [12] is a guarded command lan-
guage, based on an operation centric description, where the behavior of a system
is described as a collection of atomic operations in the form of rules. These rules
are defined by a predicate condition and the effect on the state of the system.
During execution several rules are concurrently executed in a clock cycle. Third
we consider Statecharts, which are an extension of conventional state-transition
diagrams with three elements, dealing, with hierarchy, concurrency and commu-
nication [11]. The graphical hierarchy presentation enables designers to adapt
to the required level of detail of the system. Finally, the comparison covers the
Algebra of Communicating Processes (ACP) [3]. ACP is a finite axiomatisation
based framework for specifying and manipulating the behaviour of models. It
facilitates the behavioural description for non-deterministic choices, sequential
operations, parallel composition, deadlock and communication.
7.1
Maximal Throughput
Within the specification maximal throughput is achieved by executing multiple
actions in a single clock cycle. Therefore, this comparison narrows down the
scope to the behaviour for simultaneous actions.
It is not possible to describe the simultaneous transfer of packets in TLA+
and ACP. Therefore a designer is required to apply a spatial reasoning to verify
that indeed packets are transferred simultaneously. As we compare the formalism
to mCRL2, we see that within mCRL2, it is possible to define multi-actions. We
believe that these multi-actions are more suitable for specifying the throughput
behavior as they relate better to the simultaneous packet transfers in the system.
Therefore it is not necessary for a designer to reason about multiple transitions.
For Bluespec specifications, a greedy run-time scheduler tries to acquire max-
imal throughput. It should be noted that in some cases a maximal throughput
cannot be obtained, even though all conflict-free rules are selected. To mini-
mize latency, the scheduler may chose a maximal set of actions of the design
for execution during each hardware clock cycle. Therefore it is possible that this
set does violate the maximal throughput requirement [15]. As exploration in
mCRL2 is exhaustive, and latency is no issue, maximal throughput can be guar-
anteed, by means of synchronizing actions and guards. Furthermore, although
not specified here, we believe that it possible to use the mCRL2 time operator to
enforce throughput in different ways, e.g. by enforcing the execution of actions
at predefined timestamps.
 
Search WWH ::




Custom Search