The results from our experiments with RLL are very encouraging in that we have demonstrated a composite testing and program analysis system that is practical and that finds bugs in real programs. One must keep in mind, however, that these results represent a single point in a huge design space and do not necessarily transfer to other control languages and other analysis problems. The research challenge, then, is to understand to what degree these techniques generalize.
A key idea in the RLL analysis was to combine testing and modern program analysis techniques. It is not necessarily obvious how to combine distinct analysis techniques in general. The example we have presented, which does randomized testing of an automatically generated abstraction of the program, is but one possibility. Some understanding of what combinations make sense is needed to describe the design space of composite analyses. For example, it is intriguing to consider extending our RLL analysis with model checking techniques. RLL includes timers that function as alarm clocks: a particular input wire to the timer causes the timer to wait for a constant amount of time and then write an output. The analysis described earlier models timers very crudely, thereby potentially missing some timing-dependent races. Timed automata are hybrid systems with clocks that can (among other things) cause system transitions to happen after a preset amount of time [40], which is exactly the RLL model of timers. The state reachability problem for timed automata is decidable, intuitively because there are only a finite number of possible relative orderings of timer values (i.e., which timer will go off first, second, etc.).
The decision procedure for timed automata could be incorporated into our system. The overall structure of the computation becomes a state reachability analysis, where each state corresponds to a particular configuration of timers and input values. In a particular state a full instance of the scan analysis described previously is performed. That is, in each state we evaluate multiple scans to compute the values of the outputs in that state. If there are no races in this state (i.e., the outputs stabilize), then the timer values are updated to reflect the next timer transition. Timer changes put the system in a new state, and the process repeats.
We also believe that extensive experimentation is required in our style of ``limited verification''. Programs written by people belong to a very special subset of all possible programs. To fully understand the costs and benefits of any analysis implementation and experimentation are necessary. Consider, for example, the RLL analysis with the improvements for timers just described. It is unclear whether this analysis is practical. While the analysis we have outlined is feasible to implement, the model checking component introduces a potentially exponential slowdown, as for each random initial input configuration we may explore an exponential number of states. On the other hand, even production programs appear to have relatively few timers, and so this potential state blowup may be only a theoretical possibility.