CMU-CS-06-169Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-06-169
Muralidhar Talupur November 2006 Ph.D. Thesis
Keywords: Formal methods, model checking, abstract interpretation,
abstraction, parameterized systems, cache coherence protocols, mutual
exclusion protocolsModel 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
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 This page maintained by reports@cs.cmu.edu |