Parameterized systems are systems that involve numerous instantiations of the same ÿnite-state module, and depend on a parameter which deÿnes their size. Examples of parameterized systems include sensor systems, telecommunication protocols, bus protocols, cache coherence protocols, and many other protocols that underly current state-of-the-art systems. Formal veriÿcation of parameterized systems is known to be undecidable (Inform. Process. Lett. 22 (6)) and thus cannot be automated. Recent research has shown that it is often the case that a combination of methodologies allows to reduce the problem of veriÿcation of a parameterized system into the problem of veriÿcation of a ÿnite-state system, that can be automatically veriÿed.
This paper describes several recent methodologies, based on model checking and abstraction. We start with the method of invisible auxiliary assertions that combines a small-model theorem with heuristics to automatically generate auxiliary constructs used in proofs of correctness of parameterized systems. We also describe the method of counter abstraction that o ers simple liveness proofs for many parameterized systems, and discuss novel methodologies of using counter abstraction to automatically verify that probabilistic parameterized system satisfy their temporal speciÿcations with probability 1.