Detecting Errors Before Reaching Them
Abstract
Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counter example) rather than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fall while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented which can be long before it actually occurs; for example the violation of an invariant may become unpreventable many transitions before the invariant is violated. The key observation is that "unpreventability" is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore unpreventability is inexpensive to compute for each module yet can save much work in the state exploration of the global compound system. Based on different degrees of information available about the environment we define and implement several notions of "unpreventability" including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples a distributed database protocol and a wireless communication protocol.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2000
- Accession Number
- ADA461287
Entities
People
- Freddy Y. Mang
- Luca De Alfaro
- Thomas Henzinger
Organizations
- University of California, Berkeley