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.

Le travail présenté dans ce document consiste en une approche de test fonctionnel, destinée à per- mettre la validation de systèmes hybrides pour lesquels on dispose d'une spécification composée de propriétés de sûreté. La validation consiste à vérifier que le système satisfait à sa spécification, et donc aux besoins qui motivent sa création (sous réserve que la spécification traduise correctement les besoins).

On nomme systèmes hybrides les systèmes qui intègrent des comportements continus et discrets. Leur comportement est en partie déterminé par des contraintes temporelles et/ou leur interaction avec un environnement physique via l'utilisation de capteurs et d'actionneurs. Il peut s'agir par exemple d'équipements de contrôle de procédés industriels ou de services domotiques. La validation de ces systèmes est un problème crucial, car ils sont parfois utilisés au sein d'applications où la sûreté de fonctionnement est critique (un système critique est un système dont la défaillance peut entraîner des blessures ou la mort d'êtres humains). Cette validation soulève plusieurs problèmes ; en particulier, une description détaillée du système à valider n'est pas toujours disponible, ou celle-ci est trop complexe pour qu'il soit possible en pratique d'établir avec certitude sa correction (par exemple parce que cette vérification exhaustive nécéssite des ressources en temps ou en matériel trop importantes). Dans ces conditions, nous nous intéressons à la validation de systèmes hybrides spécifiés par un ensemble de propriétés de sûreté. Une propriété de sûreté est une exigence portant sur le comportement du système qui ne contraint pas entièrement ce comportement, mais en spécifie des aspects particuliers. Elle peut ainsi porter sur la réaction attendue du système en réponse à une suite d'événements donnée, ou imposer des limites à l'évolution des grandeurs environnementales qu'il contrôle. Le travail présenté dans ce document consiste en une approche de test fonctionnel, destinée à permettre la validation de systèmes hybrides pour lesquels on dispose d'une spécification composée de propriétés de sûreté. La validation consiste à vérifier que le système satisfait à sa spécification, et donc aux besoins qui motivent sa création (sous réserve que la spécification traduise correctement les besoins). / Hybrid systems posess a continuous and discrete behavior. This behavior is partially determined by temporal constraints, and/or interactions of the system with a physical environment by means of sensors and actuators. Hybrid systems include some industrial plant control software and home automation systems. The validation of hybrid systems is a crucial problem since they may be used in safety critical applications (a safety critical system is a system whose failure may lead to unacceptable financial or human costs). This validation raises several problems; in particular a complete description of the system to be validated is not always available. Its complexity may also prevent establishing the correction of the system with certainty (if for exampl a full proof computation requires too much time or equipment). Therefore we are interested in validating hybrid systems specified by a set of safety properties. A safety property is a requirement that constrains only some aspect of the system behavior and can be fullfilled by several implementations. It may for example specify the expected reaction of the system under specific circumstances or constrain the set of values that a variable is allowed to take. The work presented in this document is a functional testing approach aimed at allowing the validation of hybrid systems for which a specification composed of hybrid safety properties is available. Validation consists in verifying that the system satisfies its specification and therefore the needs that motivated its design (assuming the specification actually matches these needs).