Compositional Analysis for Verification of Parameterized Systems

			       Samik Basu

Many safety-critical systems that have been considered by the
verification community are parameterized by the number of concurrent
components in the system, and hence describe an infinite family of
systems.  Traditional model checking can only be used for verifying
particular instances of this family. In this paper, we present a
technique based on program analysis for automatic verification of
infinite families of systems.  The technique views a parameterized system
as an expression in a process algebra (CCS) and interprets this
expression over a domain of formulas (modal mu-calculus), considering a
process as a property transformer. The transformers are constructed using
partial model checking techniques. At its core, our technique solves the
verification problem by finding the limit of a chain of formulas. We
present convergence acceleration and widening operations to find such a
limit for properties expressible in a subset of modal mu-calculus. We
describe the verification of a number of parameterized systems using our
technique to demonstrate its utility.

Joint work with C. R. Ramakrishnan.