Finding Faults Quickly in Formal Models using Random Search
David R. Owen, Tim Menzies, Mats P. E. Heimdahl, Jimin Gao · 2003
As software grows more complex, automatic verifi-cation tools become increasingly important. Unfortu-nately many systems are large enough that complete verification requires a lot of time and memory, if it is possible at all. In our preliminary studies, random search, although not a complete technique, was able to find most faults significantly faster and with less mem-ory than would be required for full verification. Here we present an experiment in which random search was used to find faults in fault-seeded models of a large com-mercial flight guidance system. To assess the perfor-mance of random search we compared it to a full ver-ification done by the model checker NuSMV. The ran-dom search results were surprisingly complete, finding nearly 90 % of the faults reported by NuSMV—and these results were generated faster and using less memory. We suggest that random search be used in conjunction with verification tools, perhaps as a fast debugging tool during model development, or even as an alternative model checking strategy on models for which the time and memory requirements would make full verification impossible. 1