Automatic State Reaching for Debugging Reactive Programs

Fabien Gaucher (1) , Erwan Jahier (1) , Florence Maraninchi (1) , Bertrand Jeannet (2)

1 VERIMAG - IMAG - VERIMAG
2 VERTECS - Verification models and techniques applied to testing and control of reactive systems

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.In this article, we 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.

Mots clés: state reaching; automated debugging of reactive programs; input sequence generation; test; counter-example generation; abstract interpretation

Domaines: Langage de programmation [cs.PL]

Fabien Gaucher, Erwan Jahier, Florence Maraninchi, Bertrand Jeannet. Automatic State Reaching for Debugging Reactive Programs. the Fifth International Workshop on Automated Debugging (AADEBUG 2003), Sep 2003, Ghent, France. ⟨hal-00000840⟩