Abstraction Techniques for Parameterized Verification
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 2006
- Accession Number
- ADA462593
Entities
People
- Muralidhar Talupur
Organizations
- Carnegie Mellon University