de Alfaro, Luca; Henzinger, Thomas AIST Austria ; Mang, Freddy Y
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.
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.
186 - 201
CAV: Computer-Aided Verification
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.