Model checking and abstraction to the aid of parameterized systems (a survey)

摘要

Parameterized systems are systems that involve numerous instantiations of the same finite-state module, and depend on a parameter which defines 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 verification 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 verification of a parameterized system into the problem of verification of a finite-state system, that can be automatically verified. 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 offers 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 specifications with probability 1.