Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Test à partir de spécifications logiques

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

Date
Le lundi 27 avril 2009 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents