gaucher03

F. Gaucher, E. Jahier, B. Jeannet, F. Maraninchi. Automatic State Reaching for Debugging Reactive Programs. In Fifth International Workshop on Automated and Algorithmic Debugging AADEBUG'2003,Ghent (Belgium), September 2003.

Download [help]

Download paper: Gziped Postscript

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

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 go the other way around; namely, given a state, obtain a sequence of inputs that leads to that state. This problem is equivalent to general safety properties verification, 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 have connected a debugger, a verification tool, and a testing tool. One of the key contributions of our proposal is the proper handling of numeric variables

Contact

Bertrand Jeannet http://www.irisa.fr/prive/bjeannet

BibTex Reference

@InProceedings{gaucher03,
   Author = {Gaucher, F. and Jahier, E. and Jeannet, B. and Maraninchi, F.},
   Title = {Automatic State Reaching for Debugging Reactive Programs},
   BookTitle = {Fifth International Workshop on Automated and Algorithmic Debugging AADEBUG'2003,Ghent (Belgium)},
   Month = {September},
   Year = {2003}
}

EndNote Reference [help]

Get EndNote Reference (.ref)