Date of Award
Master of Science
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
Bankar, Sneha, "Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers" (2014). Graduate Theses and Dissertations. 14052.