-----------------------------------------------------------------------
TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar
-----------------------------------------------------------------------

Title:   Automatic Verification of  Parameterized Systems
Speaker: Lenore Zuck

Place:   NE43-308
Time:    1-2:30pm
Date:    March 1, 2002

Abstract:

The talk discusses methodologies for automatic verification of
parameterized systems, focusing on "counter abstraction" and on
probabilistic systems.  The counter-abstraction method is
applicable to systems where each process is finite-state. A global
state of the system is abstracted by counting the number of
processes in each local state, where the counter are restricted to
none/one/some (in some cases, "one" can be omitted.)  We show to
derive a set of fairness requirements that enable automatic proofs
of liveness properties of the abstract system, from which we
conclude the corresponding property of the concrete parameterized
system.  We illustrate the method on several examples.

We then turn to the problem of automatically verifying that
probabilistic parameterized systems satisfy their 'simple'
temporal specification with probability 1.  It is based on the
observation that for such systems, probabilistic requirements can
be replaced by fairness. To verify correctness of the fair system,
we use the "network invariant" method.  We demonstrate the
methodology by providing a automatic verification of the liveness
property of Lehman and Rabin's "Courteous Philosophers" protocol.

Joint work with Amir Pnueli, Jessie Xu, and Yonit Kesten.

-----------------------------------------------------------------------