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

Fig. 2. End user perspective of the Credo Tools
between the high-level network model and the detailed component model was
checked by conformance testing. In a similar approach conformance between the
high-level network model and the detailed network model is established.
At the dataflow-level, which is the most abstract characterization of a sys-
tem, behavioral interfaces (cf. Fig. 2) are used to describe components and the
dataflow between components of a composite system. These interfaces abstract
from the details of the (object-oriented) implementation of components. Instead
they describe the components and the connections they use to communicate and
interact with each other. Credo provides as an Eclipse plug-in an integrated tool-
suite, ECT (Eclipse Coordination Tools) [13], including a plug-in for the model
checker Ve r eo fy [6,5]. Ve r eo fy uses CARML and RSL as input languages and
provides model checking of branching-time properties via a CTL -like logic with
regular expressions to specify the observable dataflow as well as alternating-time
and linear time versions thereof and bisimulation checking. The logics allow to
reason about the coordination principles and the dataflow in the network as well
as about the internal states of the components and behavioral interfaces.
The functional behavior of the objects within a component is modeled in
Creol. Furthermore, we use the timed automata of Uppaal [25,8] to create real-
time models of objects and their behavioral interfaces. The Credo tool suite offers
an automated technique for schedulability analysis of individual objects [21,20].
Given a specification of a scheduling policy (e.g., earliest deadline first) for an
object, we use Uppaal to analyze the object with respect to its behavioral
interface in order to ensure that tasks are accomplished within their specified
deadlines.