LURCH

LURCH is a software design debugging tool that uses a nondeterministic algorithm to quickly explore the reachable states of a software model. By performing a partial and random search, LURCH looks for faults in the model and reports the pathways leading to the faults.

Conventional algorithms for exploring a system's state space are deterministic, in that they have specific decision paths for mapping inputs to outputs. Nondeterministic algorithms, on the other hand, do not have such specific paths, allowing for the same inputs to result in different outputs. Deterministic analysis is often considered safer than nondeterministic methods since it explores all possible system states in an exhaustive and thorough way. Nondeterministic analysis, however, may only explore a subset of the entire state space, and thereby miss some of the possible faults.

Much evidence supports the notion of clumping, where the effective state space of a program is relatively small when compared to all reachable states. A tool such as LURCH is especially useful in such situations. However, depending on the problem, if clumping does not occur, the nondeterministic approach may not be very effective. Yet in such situations, LURCH can at least report whether performing a nondeterministic search will be safe or not.

To LURCH Or Not To LURCH

Menzies et al. in [1] argue that LURCH is not less safe than conventional deterministic algorithms for software model analysis; that LURCH is simple, competent, fast, scalable, and a stable nondeterministic analysis method:

1. LURCH is simple: The following is pseudocode for LURCH, which is considerably easier to implement compared to more complex standard model checkers.

function step(Q, state)
    while Q is not empty
        // choose a transition at random
        tr := random_pop(Q)
        // modify state vector accordingly
        execute_outputs(tr, state)
        // disqualify transitions ruled out by choice
        for tr' in same machine as tr
           delete(Q, tr')

function check(state)
    local_fault_check(state)
    deadlock_check(state)
    // cycle_check requires hash table
    cycle_check(state)

function lurch(max_paths, max_depth)
   repeat max_paths times
       // set all machines to initial state
       for m in machines
           state[m] := 0
       // generate a global state path
       repeat max_depth times
           for tr in transitions
               // see if transition is blocked
               if check_inputs(tr)
                   // if not, put it in the queue
                   push(Q, tr)
               // get next global state
               step(Q, state)
               // see if next state represents a fault
               check(state)

1. LURCH is fast: Wherease deterministic analysis tools such as NuSMV may take hours or even days to discover all faults in a design, LURCH locates the vast majority of faults in just a few minutes.

1. LURCH is competent: Though LURCH misses faults detected by slower deterministic methods, the speed with which it finds faults makes it nevertheless useful for rapid software development (where time is crucial). However, LURCH can only be effective when systems clump (though many argue that this is a frequent occurrence).

1. LURCH is scalable: For larger models, deterministic tools such as SPIN require increasingly larger amounts of resources. LURCH, on the other hand, requires only minimal more memory as problem size increases, suggesting it is not less safe than a deterministic search (where problems may be too large for the deterministic tool to handle).

1. LURCH is stable: Whereas time and memory requirements for deterministic methods can fluctuate greatly depending on the problem, LURCH has been shown to remain stable regardless of problem size. See [1] for actual measurements.

See also

• Nondeterministic
• Deterministic
• Software testing
• Software verification
• Finite state machine
• State (computer science)
• Thrash (computer science)
• Clumping

External References

[1] Menzies, Owen, Heimdahl, Gao, Cukic, Nondeterminism: Unsafe? (http://www.cs.pdx.edu/~timm/lite/readings/randomoka.pdf)