| dc.description.abstract | Web-based applications and distributed systems are ubiquitous and indispensable today. These
systems use multiple parallel machines for greater functionality, and efficient and reliable computation.
At the same time they present innumerable challenges, especially in the field of
program analysis. In this thesis, we address two problems in the domain of web based applications
and distributed systems relating to program analysis, and design effective solutions for
those problems.
The first challenge that the thesis addresses is the difficulty of analyzing a web application
in an end-to-end manner using a single tool. Such an analysis is hard due to client-server
interaction, user interaction, and the use of multiple types of languages, and frameworks in a
web application. We propose a semantics preserving modeling technique, that converts a web
application into a single-language program. The model of a web application in the thesis is a
Java program as we present our modeling technique in the context Java-based web applications.
As a result of the translation, off -the-shelf tools available for Java can now be used to analyze
the application.
We have built a tool for the translation of applications. We evaluate our translation tool
by converting 5 real world web applications into corresponding models, and then analyzing
the models using 3 popular third-party program analysis tools - Wala (static slicing), Java
PathFinder (explicit-state and symbolic model checking), and Zoltar (dynamic fault localization).
In all the analysis tools, we get precise results for most cases.
The second challenge that the thesis addresses, is the precise data
flow analysis of message
passing asynchronous systems. Message passing systems are distributed systems, where multiple
processes execute concurrently, and communicate with each other by passing messages
to the channels associated with each process. These systems encompass majority of the real
world distributed systems, e.g., web applications, event-driven programs, reactive systems, etc.
Therefore, there is a clear need for robust program analysis techniques for these systems. One
such technique is data
flow analysis, which statically analyzes a program, and approximates
the values of variables in the program due to all runs of the program, using lattices. Any precise data
flow analysis needs to account for the blocking of execution in message
passing systems, when the required message is not present in the channel. Current data
flow
analysis techniques for message passing systems either over-approximate the behavior by allowing
non-blocking receive operations, or, they are not applicable to general data
flow lattices.
The thesis proposes algorithms for performing precise data
flow analysis of message passing
asynchronous programs, using infinite, but finite height lattices. The problem was not known to
be decidable before. The algorithm builds on the concepts of parallel systems modeling theory,
in a novel and involved manner. We have also made a tool for the algorithm, and have studied
its precision and performance by analyzing 10 well-known asynchronous systems and protocols
with encouraging results | en_US |
