Stratégies Dynamiques pour la Génération de Contre-exemples - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

Stratégies Dynamiques pour la Génération de Contre-exemples

(1) , (1) , (1) , (2) , (2)


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.
Fichier principal
Vignette du fichier
rueher.pdf (336.85 Ko) Télécharger le fichier
Origin : Explicit agreement for this submission

Dates and versions

inria-00520281 , version 1 (22-09-2010)


  • HAL Id : inria-00520281 , version 1


Nguyen Le Vinh, Hélène Collavizza, Michel Rueher, Samuel Devulder, Thierry Gueguen. Stratégies Dynamiques pour la Génération de Contre-exemples. JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.207-216. ⟨inria-00520281⟩
125 View
129 Download


Gmail Facebook Twitter LinkedIn More