[Colloq] PhD Talk Tuesday February 19th

Rachel Bates rachelb at ccs.neu.edu
Mon, 18 Feb 2002 13:33:26 -0500


PhD Seminar
Tuesday February 19th
149 Cullinane Hall
4:00pm
Followed by Tea at 5pm


Speaker:  Paul Attie

Tractable Methods for the Design and Verification of  Large Concurrent
Programs

Abstract:
A concurrent program consists of some number K of sequential processes
that `interact via some mechanism such as message passing, shared
memory, or remote procedure call. Most large software systems, e.g.,
operating systems, distributed databases, networks, can be modeled as
concurrent programs.  We address the design and verification of the
synchronization and communication portion of large concurrent
programs.  Often, this portion can be implemented using a fixed,
finite amount of synchronization related data, i.e., it is
"finite-state."  Nevertheless, even when each process contains only
one bit of synchronization related data, the number of possible global
synchronization states for K processes is about 2^K, in general.
Because of this "state-explosion" phenomenon, the manual verification
of large concurrent systems typically requires lengthy, and therefore
error-prone, proofs.  Automatic verification methods (e.g., temporal
logic model checking) use state-space exploration to decide if a
system satisfies its specification, and are therefore also subject to
state-explosion.  To date, proposed techniques for ameliorating
state-explosion either require significant manual labor, or work well
only when the system is highly symmetric and regular (e.g., many
functionally similar components connected in similar ways).

Our approach structures the concurrent program so that it is a priori
easy to verify correctness. For every pair of directly interacting
components, we represent their interaction explicitly and separately
from all the other interactions in the system.  We start with a
specification (written in temporal logic) which describes all the
pairwise interactions and we automatically synthesize a "pair-system"
for each such interaction. We then "compose" the pair-systems together
to produce the final large system.  Unlike other temporal logic
synthesis techniques, our method is not subject to state-explosion
(even when all system components are functionally dissimilar), and
addresses non-functional properties such as fault-tolerance.  We also
discuss possible extensions of our work to the construction of
component-based programs.