Automatic state-reaching for debugging reactive programs
Bertrand JEANNET
Campus de Beaulieu, 35042 Rennes cedex, FRANCE

Reactive systems are made of programs that permanently interact with their environment. Debuggers generally provide support for data and state inspection, given a sequence of inputs. But, because the reactive programs and their environments are interdependent, a very useful feature is to be able to go the other way around; namely, given a state, obtain a sequence of inputs that leads to that state. This problem is equivalent to the general verification of safety properties, which is notoriously undecidable in presence of numeric variables. However, a lot of progress has been done in recent years through the development of model checking and abstract-interpretation-based techniques. We show in this talk how to take advantage of those recent advances to implement a fully automatic state reaching capability inside a debugger of reactive programs. To achieve that, we connect a debugger, a verification tool, and a testing tool. One of the key contributions of our proposal is the proper handling of numeric variables.

Slides (.pdf)