Génération automatique de cas de test guidée par les propriétés de sûreté

This work deals with the problem of the synchronous software validation against his safety properties. Safety properties allow to specify the safe software bahaviors. Generally speaking, our approach is based on the test. We define a technique to find, only from the safety properties, all data test which could lead to the violation of sefety properties. This technique allow to forcast a future violation. Different heursistics have been implemented in oder to select one data test submited to the software. These propostions are implemented inside the Lutess tool which allow to generate data test automatically and dynamically.Ce travail porte sur le problème de la validation des logiciels réactifs synchrones par rapport à des propriétés de sûreté. Les propriétés de sûreté permettent de spécifier les comportements sûrs d'un logiciel. D'une manière générale, notre approche aborde la validation par le test. Dans ce cadre, nous avons défini une technique qui permet de déterminer, à partir des propriétés de sûreté seulement, toutes les données de test favorisant l'observation d'une violation de ces propriétés. Cette technique permet d'anticiper une violation future. Différentes heuristiques ont été implantées pour sélectionner les données de test de façon efficace. Notre proposition a été intégrée à l'outil Lutess. Ce dernier est capable de générer automatiquement et dynamiquement des données de test en s'appuyant sur divers guides. La capacité de nos heuristiques à guider le test vers des situations où la propriété de sûreté peut être violée a été évaluée sur une étude de cas significative proposée par un consortium d'industriels du secteur des télécommunications