[Colloq] Reminder: PhD Thesis Proposal by Aleksandra Portnova - Today, 2pm

[Rachel Kalweit]

College of Computer and Information Science

PhD Thesis Proposal:
Aleksandra Portnova

Thesis Title:
Formal Methods for Distributed System Design via Pairwise Verification

Thursday, August 4, 2005
2:00pm
366 West Village H

Abstract
Ensuring the correct behavior of large complex systems is a key
challenge of software engineering. Due to the ineffectiveness of
testing, formal verification has been regarded as a possible approach,
but has been problematic due to the expense of carrying out large proofs
by hand, or with the aid of theorem provers.  One proposed approach to
making formal methods economical is that of automatic model-checking:
the state space of the system is mechanically generated and then
exhaustively explored to verify the desired behavioral properties.
Unfortunately, the number of global states is exponential in the number
of processes. This state-explosion problem is the main impediment to the
successful application of automatic methods such as model-checking and
reachability analysis.

My research focuses on the formulation of methods for the design of
complex distributed computing systems, and for the analysis of the
dynamic (time-varying) behavior and fault-tolerance of such systems. I
use the pairwise approach developed by Attie and Emerson, since it
overcomes state-explosion. I derive conclusions about the behavior of
the overall large system from the pairwise analysis.  Since analysis is
applied only to pairs of processes, the automatic analysis methods are
computationally efficient in my setting, whereas they have not been
computationally efficient when applied to large system as a whole.  My
work thus extends the scope of applicability of automated formal
verification methods to the design of large distributed computing
systems. I plan to further my work in the following areas:

(1) conceptually, by providing a designer with a method of decomposing a
large system so that the interactions between each pair of processes
(components) can be viewed and reasoned about in isolation from the
remaining processes (components), and  (2) computationally, by providing
automatic analysis methods and algorithms that exploit this
decomposition into ``pairs.''

Thesis Proposal Committee:
Rajmohan Rajaraman, adviser
Paul Attie,  co-adviser
Gene Cooperman
Ravi Sundaram
David Lorenz, external member
Nancy Lynch (MIT), external member




_______________________________________________
Colloq mailing list
Colloq at lists.ccs.neu.edu
https://lists.ccs.neu.edu/bin/listinfo/colloq