symbols Σ, called the action set, λ (an internal action that denotes non-observable ac-
tivity of the system) and (which denotes a successful termination) in combination
with operators. Operators in EB
3
draw their inspiration from regular expressions, the
sequential composition (), the choice (|) and the Kleene closure (
∗
), with the addition
of some operators from CSP and LOTOS: synchronization, guard, process call, and
synchronization quantification (also called indexing in CSP). The symbol 9 denotes the
interleave operator, i.e., |[∅]| . EB
3
PAI also have a guard operator and process call. The
symbol PE denotes the set of all process expressions.
It is important to note that quantification is a crucial operator in IS specification.
This constitutes a major difference from other problem domains where process algebras
are typically used (protocol specification for example). Another difference is that EB
3
is only concerned by trace equivalence. Since the main aim of EB
3
is to provide an ex-
ecutable specification, the specification style used to achieve this goal is also different.
Frappier and St.-Denis in [2] have proposed a set of rules that give EB
3
its operational
behavior. EB
3
PAI executes a specification by simply evaluating the inference rules. We
do not generate code per se; EB
3
PAI can be considered as a virtual machine and each
specification becomes a high-level program. The implementation is the combination of
EB
3
PAI and the specification.
3 Dynamic Optimization in the EB
3
PAI Interpretation Process
In [3] we provide some static optimizations. However, this is not sufficient to yield
efficient interpretation. To provide a useful tool, we need to optimize other aspects of
the interpretation algorithm, primarily to reduce the time and space complexity for large
quantifications.
3.1 Optimization of Process Expression Storage in Memory
During an execution, actions and process expressions can be copied several times. Some
execution sequences can require a large amount of memory. The two main causes are
quantification and choice resulting in the execution of some non-deterministic specifi-
cations. In order to minimize memory space, process expressions can be represented by
a graph which allows them to be shared. For instance, if E
1
is a sub-expression of both
E
2
and E
3
, than E
1
can be instantiated once and referenced by both E
2
and E
3
.
3.2 Optimizing Quantification Execution Time: Direct κ-optimization
The EB
3
language allows the use of quantification operators. A basic approach to ex-
ecuting quantification operators is too ineffective to be acceptable. To optimize these
executions, we determine by static analysis of each quantified expression which value
of the quantified set must be selected based on the parameters of the action to exe-
cute. We call these values κ-values, the positions of the values in the action parameters
κ-positions, and this method direct κ-optimization.
This approach is sufficient to optimize a choice quantification, since the quantifica-
tion disappears after the transition. In the case of a quantified interleave, the quantifica-
tion remains in the result process expression, since it can spawn one interleave process
190