Detecting Errors Before Reaching Them
CALIFORNIA UNIV BERKELEY DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
Pagination or Media Count:
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.
- Numerical Mathematics
- Operations Research