Abstract
The thesis is part of the Creol research project, and considers objects
that communicate asynchronously through message passing. Objects and messages
are represented by a global state called a configuration. The
configuration is a multiset that models a highly non-deterministic system with
concurrent objects. This model is well suited for both standard object
based Maude specifications and Creol programs executed in Maude by the
Creol interpreter.
The objects' interaction can be recorded by an external
observer in a communication history. By specifying predicates
on this history, we can define invariants for an object's behavior, as well as
an object's assumptions with regards to the behavior of its surrounding
environment.
The main goal for this thesis is to develop a formal framework in
Maude for executing specifications modeling distributed systems, that can record and utilize a communication history. More specifically, the following
points are addressed:
- How can we execute Maude specifications and transparently, in the
sense that the original specification remains unchanged, build a
communication trace as the execution proceeds?
- How can we define predicates on this trace, and use such predicates
to control and test the behavior of objects?
- How can these techniques be applied to the Creol language, and more
specifically, to the Creol interpreter developed in Maude?
- How can we execute models of highly non-deterministic concurrent
systems, such as Creol programs, in the deterministic rewrite tool
Maude?