The thesis is part of the Creol research project, and considers objectsthat communicate asynchronously through message passing. Objects and messagesare represented by a global state called a configuration. Theconfiguration is a multiset that models a highly non-deterministic system withconcurrent objects. This model is well suited for both standard objectbased Maude specifications and Creol programs executed in Maude by theCreol interpreter.
The objects' interaction can be recorded by an externalobserver in a communication history. By specifying predicateson this history, we can define invariants for an object's behavior, as well asan object's assumptions with regards to the behavior of its surroundingenvironment.
The main goal for this thesis is to develop a formal framework inMaude for executing specifications modeling distributed systems, that can record and utilize a communication history. More specifically, the followingpoints are addressed:
- How can we execute Maude specifications and transparently, in thesense that the original specification remains unchanged, build acommunication trace as the execution proceeds?- How can we define predicates on this trace, and use such predicatesto control and test the behavior of objects?- How can these techniques be applied to the Creol language, and morespecifically, to the Creol interpreter developed in Maude? - How can we execute models of highly non-deterministic concurrentsystems, such as Creol programs, in the deterministic rewrite toolMaude?