[Colloq] PhD Thesis Proposal by Aleksandra Portnova - Thursday, Aug. 4

[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