Abstract

Monitoring and checking the execution of a distributed program incur significant overhead due to the large number of states that need to be considered when using interleaving semantics to model the concurrency. In this thesis, we use partial order semantics in modeling a distributed computation. Specifically, a Pomset automaton model is used to specify all the allowable partial orders of a given design. The distinct aspects of requirement are separately modeled: the ordering requirements among atoms (a set of source code statements that are expected to be performed atomically) and the correctness of each atom. And atomization is introduced into the abstraction to map the correspondence between events in the design layer and events in code space. Therefore, ordering requirements are specified among the so called abstract atoms; then, these atoms in the design space are mapped into the code space using atom variables. The correctness of an atom is specified by using predicates on a state that is reached upon the completion of an atom. In our Pomset model, the ordering is explicit and easily checkable, which is different from the more traditional model checking. The proposed methodology is mechanized in a runtime verification tool on a multi-agent platform (Jade) to demonstrate its effectiveness. The runtime verifier accepts a user-specified Pomset automaton and the associated atom predicates for a given Jade source program. Implemented in AspectJ, the verifier monitors and checks both ordering requirements and atom requirements on-the-fly, and echoes appropriate results to the user for debugging and testing.