On the advantages of approximate vs. complete verification: bigger models, faster, less memory, usually accurate

摘要

We have been exploring LURCH, an approximate (not necessarily complete) alternative to traditional model checking based on a randomized search algorithm. Randomized algorithms like LURCH have been known to outperform their deterministic counterparts for search problems representing a wide range of applications. The cost of an approximate strategy is the potential for inaccuracy. If complete algorithms terminate, they find all the features they are searching for. On the other hand, by its very nature, randomized search can miss important features. Our experiments suggest that this inaccuracy problem is not too serious. In the case studies presented here and elsewhere, LURCHS random search usually found the correct results. Also, these case studies strongly suggest that LURCH can scale to much larger models than standard model checkers like NuSMV and SPIN. The two case studies presented in this paper are selected for their simplicity and their complexity. The simple problem of the dining philosophers has been widely studied. By making the dinner more crowded, we can compare the memory and runtimes of standard methods (SPIN) and LURCH. When hundreds of philosophers sit down to eat, both LURCH and SPIN can find the deadlock case. However, SPINS memory and runtime requirements can grow exponentially while LURCHS requirements stay quite low. Success with highly symmetric, automatically generated problems says little about the generality of a technique. Hence, our second example is far more complex: a real-world flight guidance system from Rockwell Collins. Compared to NuSMV, LURCH performed very well on this model. Our random search finds the vast majority of faults (close to 90%); runs much faster (seconds and minutes as opposed to hours); and uses very little memory (single digits to 10s of megabytes as opposed to 10s to 100s of megabytes). The rest of this paper is structured as follows. We begin with a theoretical rationale for why random search methods like LURCH can be incomplete, yet still successful. Next, we note that for a class of problems, the complete search of standard model checkers can be overkill. LURCH is then briefly introduced and our two case studies are presented.