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

channel leading back to the initial location. The implementation of the openCS
method involves sending a message confirmCS back to the sender, while the register
method is modeled merely as a time delay.

Checking Schedulability. When an object is instantiated, an off-the-shelf
scheduler is selected and tailored to the particular needs of the object. For an
object, we get a network of timed automata in Uppaal by instantiating the au-
tomata templates for methods, behavioral interface and the scheduler. There are
two conditions indicating that a system is not schedulable:

1. The scheduler receives a new message when the message queue is already full.
In theory [20], a schedulable object needs a queue length of at most

,where d max is the biggest deadline value used and b min is the
smallest execution time of all methods.
2. The deadline of at least one message in the queue is missed.

d max /b min

In either of the above cases, the scheduler automaton goes to a location called
Error . This location has no outgoing transitions and therefore causes deadlock.
Therefore, absence of deadlock implies schedulability, as well as correct output
behavior for the object.
Due to the high amount of concurrency in the model, model checking is of lim-
ited use. Nevertheless, we can use the simulation feature of Uppaal [29] to analyze
bigger systems. We measure the worst-case response time for each message, which
identifies a lower bound for the deadline value in a schedulable system.

5 Conclusions

We presented an extended version of the Credo methodology now covering also the
detailed modeling and analysis of the network. The Credo modeling and analysis
techniques addressing highly reconfigurable distributed systems presented cover
a broader spectrum of the software development process. The Ve r eo fy tool set
is added to the picture providing modeling and analysis techniques for detailed
network models.
At a high level of abstraction, the dynamic connections between the components
are modeled using behavioral interface specifications. The detailed model of the
network is given in terms of a Reo model specified in Ve r eo fy . The detailed model
of the components is given in terms of an object-oriented Creol model. Both models
are used for analysis of functional as well as non-functional properties, e.g.,
schedulability, deadlock freedom. The conformance between the component and
the network models is established via the behavioral interface specifications. Fur-
thermore we can establish conformance between the Creol model and a given im-
plementation by conformance testing.
The process described in this paper can be integrated in the existing software
development methodologies which support component-based modeling, and thus
enhance them with support for formal modeling and analysis of dynamically re-
configurable distributed systems. In the future, we intend to broaden the scope