Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Gziped Postscript (.ps.gz)
Copyright noticeThis 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.
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.
Bertrand Jeannet
Bertrand.Jeannet@irisa.fr
@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}
}
Get EndNote Reference (.ref)