The Credo Methodology - Formal Methods for Components and Objects - page 44

Conformance between a model of a component implementation and its behav-
ioral interface specification is checked by the Credo tools [17]. Moreover, given
an implementation of a component in a programming language like C, Credo
also provides a technique to check conformance between the implementation
and the Creol model [18,1]. Both techniques are based on testing .Theabstract
behavioral interface model is used to generate test cases to steer the execution.
To illustrate the Credo methodology we will give a running example. Through-
out the paper we model and analyze a file-sharing system with hybrid peer-to-
peer architecture (like in Napster), where a central server keeps track of the data
in every peer node.
In Section 2, we develop the structural and behavioral interfaces of the com-
ponents (peer nodes of the P2P system) and the network (the network manager
managing the dynamic connections between peer nodes); and prove some ex-
ample properties of different kinds. In Section 3, we give a detailed model of
the network using the Ve r eo fy tool suite and analyze it by means of simulation
and model checking. In Section 4, we give executable object-oriented models
for the components and analyze them by means of simulation and testing for
conformance both with respect to the behavioral interfaces and a Creol im-
plementation. We demonstrate schedulability analysis by analyzing the central
server of the peer-to-peer example. Section 5 concludes the paper.

2 High-Level Dataflow Model

We use the exogenous coordination language Reo [3] for the high-level dataflow
modeling. Reo is a channel-based formalism that supports compositional design
of the network that yields the glue-code for a given set of components. In Reo,
a system consists of a set of components connected by a network. The network
exogenously controls the dataflow between the components and may be dynami-
cally reconfigured to alter the connections between the components. At this level
of abstraction, only a facade of each component is visible. A facade consists of
port and event declarations, and its abstract behavior is specified using an au-
tomata model called constraint automata [7]. Constraint automata are variants
of labeled transition systems where the transitions are labeled by sets of read
and write operations on I/O-ports of components and dataflow locations of the

sReq cReq
N1
sAns cAns

sReq cReq
N3
sAns cAns

sReq cReq
N2
sAns cAns

Fig. 3. Peer nodes in the P2P system