Information Technology Reference
In-Depth Information
E{theAnswerOut[0], theAnswerOut[1], theAnswerOut[2]}
G["Manager.release_buffer.state==EMPTY"]
All properties that have been presented in this section have successfully been
validated for our model of the peer-to-peer network for which the full source code
is available on the web [30]. Besides model checking for temporal logics,
Ve r eo fy
supports checking bisimilarity of two automata, e.g., that two implementations
of the network manager are bisimilar.
4 Object-Oriented Model of the Components
In this section, we model the components in Creol, an executable modeling lan-
guage. To model the components, we provide interfaces for the intra-component
communication and a Creol implementation of the components. Together with
a Creol implementation of the network manager, we get an executable model
of the whole system. Since Creol models are executable we use the terms Creol
model and Creol implementation interchangeably.
We use intra-component interfaces together with the behavioral interfaces of
Section 2.2 to derive test specifications to check for conformance between the
behavioral models and the Creol implementation. We also use this specification
to simulate the environment of a component while developing the component.
Given a C implementation of the system, we use the behavioral interfaces of
Section 2.2 to derive test scenarios for checking conformance between the Creol
model and an implementation in an actual programming language. Dynamic
symbolic execution on the Creol implementation is used to compute test inputs
for the scenarios for an improved coverage of the model [18].
Finally, we model the real-time aspects of the system using timed automata. In
the real-time model, we add scheduling policies to the objects. Here, we check for
schedulability, i.e., whether the tasks can be accomplished within their deadlines.
4.1 Modeling in Creol
Creol is an executable modeling language suited for distributed systems. Types
are separated from classes, instead (behavioral) interfaces are used to type ob-
jects. Objects are concurrent, i.e., conceptually, each object encapsulates its own
processor. Creol objects can have active behavior, i.e., during object creation a
designated
run
method is invoked.
Creol allows for flexible object interaction based on asynchronous method
calls, explicit synchronization points, and underspecified (i.e., nondeterminis-
tic) local scheduling of the processes within an object. Creol supports software
evolution by means of runtime class updates [31]. This allows for runtime re-
configuration of the components. To facilitate the exogenous coordination of
the components we have extended Creol with facades and an event system (cf.
Section 2.1).
The modeling language is supported by an Eclipse modeling and analysis
environment which includes a compiler and type-checker, a simulation platform
