Information Technology Reference
In-Depth Information
requested data from its
req
port. The server looks up the data corresponding to
the
key
in the data-store using the
find
operation. The result is sent back on the
ans
port. The event
closeSS
announces the accomplishment of the transaction.
Finally, the server prepares for a new session by calling the
run
method again.
4.2 Analysis of the Model
Creol programs and models can be
executed
using the rewriting logic of Maude
[12]. Maude offers different modes of rewriting and additional capabilities for
validation, e.g., a search command and the means for model checking. Credo
offers techniques to analyze
parts
of the system in isolation; on the lowest level,
to analyze the behavior of a single (active) object in isolation.
Credo offers techniques to analyze, in a black-box manner, the behavior of a
component modeled in Creol, by interaction via message passing. This allows for
the description and analysis of systems in a divide-and-conquer manner. Thus
the developer has the choice of developing the system bottom-up or top-down.
Although Creol allows modeling systems on a high level, the complete model
might still be too large to be analyzed or validated as a whole. By building upon
the analysis of the individual components, compositional reasoning still allows
us to validate the system.
Conformance Testing of the Model.
In the context of the Creol concurrency
model, especially the
asynchrony
poses a challenge for validation and testing.
Following the black-box methodology, an abstract component
specification
is
given in terms of its interaction with the environment. However, in a particular
execution, the actual order of outputs issued from the component may not be
preserved, due to the asynchronous nature of communication. To solve this prob-
lem, the conformance of the output to the specification is checked only up-to a
notion of observability [17].
The existing Creol interpreter is combined with an interpreter for the abstract
behavior specification language to obtain a
specification-driven interpreter for
testing and validation
[17]. It allows for
run-time assertion checking
of the Creol-
models, namely for compliance with the abstract specification.
We derive a specification for an object directly from the structural interfaces
and the behavioral interfaces. The specification of the implementation of the
ServerSide
is derived from the facade depicted in Section 2.1 and the behavioral
interface depicted in Section 2.2. The facade determines the direction of a com-
munication, i.e., whether it is incoming or outgoing communication. For the spec-
ification the direction is inverted - the specification 'interacts' with the object to
analyze it. The order of the events is determined by the behavioral interface.
The specification language features, among others, choice (between communi-
cation in the same direction, i.e., incoming only or outgoing only) and recursion.
As an example, we give the specification of a server:
ϕ
S
=
event
register
(
keyList
)
?
.
rec
X.
event
openSS
()
?
.
port
s.sReq
(
key
)
!
.
port
s.sAns
(
data
)
?
.
event
closeSS
()
?
.X
