LSV Seminar

Date

Monday, April 27 2009 at 11:00AM

Place

Salle de Conférence (Pavillon des Jardins)

Speaker

Delphine Longuet (LSV, ENS Cachan, CNRS)

Le test est l'une des méthodes les plus utilisées pour la validation des syst-bèmes informatiques. Lorsque l'implantation du système -Aà tester n'est pas connue, les tests sont sélectionnés et construits à partir d'une spécification (formelle) du syst-bème. Il existe principalement deux approches du test -Aà partir de spécifications formelles : les spécifications logiques sont utilisées pour tester le comportement fonctionnel des syst-bèmes (les donn-Aées), tandis que les syst-bèmes de transitions sont utilis-Aés pour tester le comportement dynamique et réactifs des syst-bèmes (actions et communications).

-A Une théorie du test à partir de spécifications logiques a été définie dans les années 90, formalisant le cadre de test ainsi que les différentes phases du processus de test. Ces travaux proposent en particulier une méthode de sélection de tests appelée dépliage pour des spécifications de forme restreinte dont les axiomes sont des équations conditionnelles. L'idée de cette méthode est d'utiliser des techniques de preuve afin de guider la sélection de tests. Le but est d'obtenir une couverture pertinente des comportements du syst-bème.

-A Je présenterai tout d'abord cette formalisation du test, en particulier le probl-bème de l'existence d'un jeu de tests exhaustif, puis la m-Aéthode de sélection de tests par dépliage. Je présenterai ensuite deux aspects de mes travaux : - la généralisation de ce cadre de test aux spécifications du premier ordre, et en particulier les résultats d'exhaustivité et de complétude de la sélection par dépliage étendue à ces spécifications - l'adaptation de ce cadre, ainsi que les résultats d'exhaustivité et l'adaptation du dépliage, à des spécifications modales du premier ordre, dans le but de proposer une nouvelle approche de test pour les syst-bèmes r-Aéactifs.