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
Copyright Date
2014
Language
en
File Format
application/pdf
File Size
93 pages
Recommended Citation
Bankar, Sneha, "Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers" (2014). Graduate Theses and Dissertations. 14052.
https://lib.dr.iastate.edu/etd/14052
