Degree Type

Thesis

Date of Award

2014

Degree Name

Master of Science

Department

Computer Science

First Advisor

Samik Basu

Abstract

Model Checking of distributed systems which communicate via message exchanges

is an open research problem. Such communication results in asynchronous interaction

between senders and receivers, one where the communicating entities, do not move in

lock-step. Model Checking is only possible for systems which can be represented as

finite state systems. Distributed Systems which communicate asynchronously cannot be

represented as finite state systems due to undefined bound on the message buffers meant

for message exchanges. Thus in general model checking such systems is undecidable.

In this thesis, we present a technique to automatically identify asynchronous systems

whose interactions can be represented by some finite state systems. This will allow us

to automatically model check the asynchronous systems. We also present a prototype

implementation and discuss the application of our technique on several case studies from

existing literature.

Copyright Owner

Sneha Bankar

Language

en

File Format

application/pdf

File Size

93 pages

Share

COinS