Information Technology Reference
In-Depth Information
To test our executable model
ServerImpl
for conformance with respect to the behav-
ioral interface description, we translate the specification to Creol and in the next
step to Maude. The specification in Maude is executed together with the model.
With the data-store at hand, we specify via the method parameters that the data
delivered along the
sAns
port of the server is actually the data identified by the key.
This needs to be done on the level of the Maude code.
The object is executed together with the specification in a special version of
the Maude interpreter customized for the testing purpose. The programmer can
track down the reason for a problem according to the Maude execution. This can
be either a mistake in the executable model or a flaw in the behavioral model,
i.e., the specification. The interpreter reports an error if unexpected behavior is
observed, i.e., an unspecified communication from the object to the specification,
or a deadlock occurs.
Simulation.
The conformance testing introduced in the previous section is al-
ready a simulation of a part of the system, i.e., the object under test. We use a
modified version of the above testing interpreter to eliminate the error reporting.
Notice that the Maude interpreter of Creol is a set of rewrite rules which reduces
the modification of the interpreter in this case to the deletion of the rules dealing
with the error reporting.
Furthermore, we use the facades and behavioral interfaces of section 2 to derive
a Creol skeleton of the network. By filling in the details of the network manager,
we get a Creol model of the network. The model of the network and the models of
the components together form a model of the entire system, which can be executed
in Maude.
We use Maude to steer the execution of the model on different levels. We use
the different built-in rewriting strategies to simulate different executions of the
system. We use Maude's search command to search for a specific execution lead-
ing to a designated program state. And we use Maude's meta-level to control an
execution by controlling the application of the rewrite rules.
To supplement the above simulation strategies, we use Maude's
model-checking
facilities. In general, the simulation is non-deterministic, which means, that only
part of the specified behavior is covered. Therefore erroneous behavior might be
missed. Maude's search facility allows us to explore the search space systemati-
cally. A general limitation of model checkers is the state space explosion, which
makes larger systems unmanageable, when it comes to model checking. By ana-
lyzing
parts
of the system in isolation we reduce the state space explosion. Fur-
thermore, Creol as a modeling language allows us to represent the system in a
high-level, abstract manner, and concentrate on the crucial design-choices, which
furthermore increases the chances of being able to model-check such a model. Since
Maude is based on rewriting, dealing with the asynchronous nature of communi-
cation is natural: the asynchronicity is represented by trace-equivalence, which
is directly represented as equivalence in the Maude rewriting system. This allows
the execution engine to more eciently represent the state space (by working on
the normal forms instead of exploring all re-orderings one by one).
