Login | Register

Design and implementation of a Pomset automaton based runtime verifier for distributed Jade programs

Title:

Design and implementation of a Pomset automaton based runtime verifier for distributed Jade programs

Liu, Yan (2008) Design and implementation of a Pomset automaton based runtime verifier for distributed Jade programs. Masters thesis, Concordia University.

[img]
Preview
Text (application/pdf)
MR42533.pdf - Accepted Version
2MB

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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (Masters)
Authors:Liu, Yan
Pagination:xi, 88 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M. Comp. Sc.
Program:Computer Science and Software Engineering
Date:2008
Thesis Supervisor(s):Jayakumar, Rajagopalan and Li, Hon Fung
ID Code:975995
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 16:18
Last Modified:18 Jan 2018 17:41
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top