Contexte : Le test de conformité est un test de type boîte noire. On se
donne une spécification d'un système ouvert qui sert de modèle de référence et
une implémentation réelle de ce système (implementation under test ou IUT) dont
on ne connait le comportement que par ses interactions avec l'environnement. Un
test consiste à stimuler l'IUT par des événements émis par un testeur, à
observer les réactions de l'IUT, et à en déduire la correction ou non de l'IUT
par rapport à sa spécification en fonction d'une relation de conformité.
L'outil TGV, développé dans le projet, permet de générer automatiquement les
cas de test correspondant à une spécification et un objectif de test donné.
Sujet : Nous proposons ici de prendre une approche complémentaire, qui
est de vérifier formellement des cas de test existants. En effet, dans la
pratique industrielle, les cas de test sont encore souvent écrits ``à la
main'', et la complexité du processus fait que presque inévitablement des
erreurs sont introduites. La démarche proposée est de définir formellement ce
qu'est un cas de test (associé à une spécification et à un objectif de test
donnés) et d'utiliser un prouveur de théorèmes (PVS) pour vérifier qu'un cas de
test donné satisfait à la définition. Des stratégies de preuves seront
implémentées, qui viseront à automatiser au maximum le processus de preuve.
Idéalement, la preuve sera entièrement automatique pour les spécifications
finies, et fortement assistée pour les spécifications à espace d'états infini.
Dans le cadre de ce stage on se limitera au cas des spécifications finies,
laissant le cas général pour un travail de thèse dans lequel le DEA devrait
déboucher.