Projects

The Nimbus Environment

Formal Verification--Model Checking

Formal Verification--Theorem Proving

Refutation using Random Search

Modeling Methodology

Specification Centered Testing

Statistical Testing

Correct Code Generation

CriSys Home

CS Home

Refutation and Debugging – Random Search

Automatic verification by model checking has been effective in many domains including computer hardware design, networking, security and telecommunications protocols, automated control systems and others.  Many real-world software models, however, are large enough that full verification requires much time and memory, if full verification is possible at all.  Incomplete, but faster state-space exploration techniques, capable of finding errors but not formally proving their absence, are useful for faster feedback during development.

As a starting point, we choose to evaluate the effectiveness of a purely random state-space exploration strategy on industrial sized software models in terms of performance and fault-finding ability.  In these experiments we compare full verification with the NuSMV model checker and a random search tool LURCH, developed at West Virginia University, which implements an efficient random state search algorithm based on AND-OR graphs. 100 individual faults of four different types were automatically injected into a Flight Guidance System (FGS) RSML^-e specification using the NIBUS Fault Seeder. The SMV specifications translated from these faulty RSML^-e models, in combination with a verification suite of more than 200 CTL temporal properties, generated 155 property violations.  When the RSML^-e models and properties involved in the violations were translated into the LURCH input specifications and evaluated with LURCH, in 5 test runs with 30 minute cut-offs and non-optimized search parameters, 85% of the property violations were found in at least one run and 68% were found consistently in all five runs.  In total, 89% of the faults were found by LURCH.   Furthermore, the vast majority of these violations were found in the first several minutes of the test runs.  In comparison, the full verification by NuSMV typically took an hour or two, and in the worst case, took over 36 hours.  These results strongly suggest that a simple, incomplete random state search strategy is able to find the majority of the faults significantly faster than full verification, yet a small portion of the faults may take disproportionally large effort to find.   Therefore, random search may 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 the models for which the time and memory requirements would make full verification impossible.