LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

Test à partir de spécifications logiques

Visit website for this news | Export event in iCalendar format

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.


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Feb 19

Past seminars