| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Stratégies Dynamiques pour la Génération de Contre-exemples
Abstract : Checking safety properties is mandatory in the vali- dation process of critical software. When formal verica- tion tools fail to prove some properties, testing is neces- sary. Generation of counterexamples violating some pro- perties is therefore an important issue, especially for tri- cky programs the test cases of which are very difficult to compute. We propose in this paper dierent constraint based dynamic strategies for generating structural test cases that violate a post-condition of C or JAVA pro- grams. These strategies have been evaluated on stan- dard benchmarks and on real applications. Experiments on a real industrial Flasher Manager controller and on the public available implementation of the Traffic Col- lision Avoidance System (TCAS) show that our system outperforms state of the art model checking tools like CBMC or constraint based test generation systems like Euclide.
Cited literature [21 references]
https://hal.inria.fr/inria-00520281
Contributor : Christophe Lecoutre <>
Submitted on : Wednesday, September 22, 2010 - 6:26:20 PM
Last modification on : Wednesday, October 14, 2020 - 4:24:16 AM
Long-term archiving on: : Thursday, October 25, 2012 - 11:21:02 AM
Contributor : Christophe Lecoutre <>
Submitted on : Wednesday, September 22, 2010 - 6:26:20 PM
Last modification on : Wednesday, October 14, 2020 - 4:24:16 AM
Long-term archiving on: : Thursday, October 25, 2012 - 11:21:02 AM
File
rueher.pdf
Explicit agreement for this submission