A Meta-Level Framework for Recording and Utilizing Communication Histories in Maude

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?