Detecting errors before reaching them

L. De Alfaro, T.A. Henzinger, F. Mang, in:, Springer, 2000, pp. 186–201.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published
Author
; ;
Series Title
LNCS
Abstract
Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) 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 fail, 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.
Publishing Year
Date Published
2000-01-01
Acknowledgement
This research was supported in part by the DARPA (NASA) grant NAG2-1214, the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, the DARPA (MARCO) grant MDA972-99-1-0001, and the NSF CAREER award CCR-9501708.
Volume
1855
Page
186 - 201
Conference
CAV: Computer-Aided Verification
IST-REx-ID

Cite this

De Alfaro L, Henzinger TA, Mang F. Detecting errors before reaching them. In: Vol 1855. Springer; 2000:186-201. doi:10.1007/10722167_17
De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). Detecting errors before reaching them (Vol. 1855, pp. 186–201). Presented at the CAV: Computer-Aided Verification, Springer. https://doi.org/10.1007/10722167_17
De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “Detecting Errors before Reaching Them,” 1855:186–201. Springer, 2000. https://doi.org/10.1007/10722167_17.
L. De Alfaro, T. A. Henzinger, and F. Mang, “Detecting errors before reaching them,” presented at the CAV: Computer-Aided Verification, 2000, vol. 1855, pp. 186–201.
De Alfaro L, Henzinger TA, Mang F. 2000. Detecting errors before reaching them. CAV: Computer-Aided Verification, LNCS, vol. 1855. 186–201.
De Alfaro, Luca, et al. Detecting Errors before Reaching Them. Vol. 1855, Springer, 2000, pp. 186–201, doi:10.1007/10722167_17.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar