Information Technology Reference
In-Depth Information
Conformance Testing of the Implementation.
The testing process uses for-
mal methods (e.g., automata and simulation of a model's formal program seman-
tics) to provide the necessary links between behavioral interfaces, Creol models,
and the actual implementation.
Behavioral interfaces provide
test scenarios
, patterns of interactions between
the components. A test case created according to a test scenario represents a func-
tional description, but does not guarantee a good coverage of the model. To opti-
mize the coverage,
dynamicsymbolicexecution
is used to analyze execution paths
through the Creol model to find representative test cases while avoiding redun-
dancies in the test suite [18].
Once a test suite is created, the next step in testing is executing the tests on
the implementation and reaching a test verdict to check the conformance between
model and implementation. Testing a concurrent system involves validation of
both functional and non-functional aspects. Functional aspects are covered by
standard techniques like runtime assertions in the implementation and unit test-
ing. To test the concurrency behavior of an implementation against its model we
use the observation that typically the Creol model and the implementation share a
common structure with regard to high-level structure and control flow. It is there-
fore reasonable to assume that, given equivalent stimuli (input data), they will
behave in an equivalent way with regard to control flow.
We instrument the implementation to record
events
and use the instrumented
implementation to record
traces
of observable events. Then we restrict the exe-
cution of the model to these traces. If the model can successfully play back the
trace recorded from the implementation (and the implementation produces the
correct result(s) without assertion failures), then the test case is successful. The
Creol model is used as a test oracle for the execution of the test cases on the actual
implementation [1].
4.3 Schedulability Analysis
In this section, we explain how to model the real-time aspects of the peer-to-peer
system using timed automata and the Uppaal model checker [25]. An object or
component is called schedulable if it can accomplish all its tasks in time, i.e., within
their designated deadlines. We demonstrate the schedulability analysis process
[14,20] on the network manager object in the peer-to-peer model, which is the
most heavily loaded entity in this system.
In the real-time model of an object, we add explicit schedulers to object specifi-
cations. For schedulability analysis, the model of an object consists of three parts:
the behavioral interface, the methods and the scheduler.
Behavioral interface.
To analyze an object in isolation, we use the behavioral
interface as an abstract model of the environment. Thus, it triggers the object
methods. Fig. 13 shows the behavioral interface of the network manager
augmented with real-time information. The automata in this figure are derived
from the behavioral interface of Peer (see Section 2.2) by removing the port
operations. To send messages, we use the
invoke
channel, with the syntax
