LURCH is a tool for software design debugging 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.
Contents |
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 (computer science), where the effective state space of a program is small 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.
Menzies et al. in [1] argue that LURCH is no less safe than conventional deterministic algorithms for software model analysis; that LURCH is simple, competent, fast, scalable, and a stable nondeterministic analysis method:
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)