Model checking is a well known formal verification technique that has been particularly successful for finite state systems such as hardware systems. Model checking essentially works by a thorough exploration of the state space of a given system. As such, model checking is not directly applicable to systems with unbounded state spaces like parameterized systems. The standard approach for applying model checking to unbounded systems is to extract finite state models from them using conservative abstraction techniques. Properties of interest can then be verified over the finite abstract models.

In this thesis, we propose a novel abstraction technique for model checking parameterized systems. Parameterized systems are systems with replicated processes in which the number of processes is a parameter. This kind of replicated structure is quite common in practice. Standard examples of systems with replicated processes are cache coherence protocols, mutual exclusion protocols, and controllers on automobiles. As the exact number of processes is a parameter, the system is essentially an unbounded system. The abstraction technique we propose, called environment abstraction, tries to simulate the way a human designer thinks about systems with replicated processes. The abstract models we construct are easy to compute and powerful enough to verify properties of interest without giving any spurious counterexamples. We have applied this abstraction method to several well known parameterized systems like cache coherence protocols and mutual exclusion protocols to demonstrate its efficacy. Importantly, we show how to remove a commonly used, but severely restricting assumption, called the atomicity assumption, while verifying parameterized systems.

We also apply insights from environment abstraction in a slightly different setting, namely, that of systems consisting of identical processes placed on a network graph. Adapting principles from environment abstraction, we show how the verification of a system with a large network graph can be decomposed into verification of a collection of systems, each with a small constant sized network graph. As far as we are aware, ours is the first result to show that verification of systems with complex network graphs can be decomposed into smaller problems.

280 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu