Elisangela Rodrigues Vieira

• Génie Logiciel
• Modèles Formels
  
• Validation des systèmes
• Protocole réseau
• Systèmes temporisés
• Génération automatique des cas de tests
• Objetives de test
• Exécution symbolique
  
• Informatique appliqué au domaine de la santé
  

Son parcours...

• Thèse: "Automated Model-based Test Generation for Timed Systems" (.zip)

Soutenue le 9 juillet 2007, à l'INT, Evry/FR
Mention: Très Honorable
Directrice de thèse: Prof. Ana Cavalli

Membres du Jury:
Richard Castanet, Professeur, Université de Bordeaux I, Bordeaux/FR.
Ismael Rodriguez, Professeur,  Universidad Complutense de Madrid (Espagne).
Jean-Pierre Gallois, Ingénieur Chercheur au CEA/Saclay, Gif-sur-Yvette/FR.
Eliane Martins, Professeur, Universidade Estadual de Campinas (Brésil).
Fatiha Zaidi, Maître de Conférences, Université de Paris Sud XI, LRI, Orsay/FR.
Ana Cavalli, Professeur, Institut National des Télécommunications, Evry/FR.



Abstract
Timed Systems are systems with real-time constraints. The correctness of a timed system depends not only upon the operations it  performs but also the timing when they are performed. The aim of testing a system is to guarantee its correctness. Model-based test generation is an approach to generate test cases based on a formal model. Although test generation methods have long existed, its timed counterpart is still a new field. In addition, most of the proposed solutions suffer from combinatory explosion which continues to limit their applicability in practice. Accordingly, it explains why there are so few automatic formal methods for testing generation, for both time and untimed systems.

This thesis presents an automatic test generation approach which addresses timed systems using a test-purpose algorithm. This test purpose approach guarantees the generation of test cases with regard to critical parts of the system while avoiding the state explosion problem. In addition, we propose techniques to generate test sequences with timing-fault detection and with delayed and/or instantaneous transitions. In order to evaluate the applicability and efficiency of the proposed method, we have implemented two prototype tools: one based on an industrial simulator for SDL specifications and another using a free toolset based on IF models.

Résumé
Les systèmes temporisés sont des systèmes avec des contraintes de temps réel. L'exactitude d'un système temporisé dépend non seulement des opérations qu'il effectue mais également de leur synchronisation quand ils sont exécutés. La synchronisation prend en compte l'ordre des opérations mais surtout le moment où elles sont exécutées.

Tester un système vise à garantir son exactitude. La génération de tests basée sur des modèles est une approche pour produire des cas de tests basés sur un modèle formel. Bien que d'autres méthodes de génération de tests aient déjà été proposées, la génération pour les systèmes temporisés est un domaine bien plus récent. En outre, la plupart des solutions proposées souffrent de l'explosion combinatoire, ce qui limite toujours leur applicabilité dans la pratique. Par conséquent, cela explique pourquoi il y a si peu de méthodes formelles automatiques pour la génération de tests dans tous les domaines.

Cette thèse présente une approche automatique de génération de tests adressée aux systèmes temporisés. Pour cela, nous proposons un algorithme de génération basé sur des objectifs de tests. Cette approche permet de générer des tests pour ce qui concerne les parties critiques du système et évite le problème d'explosion combinatoire. En outre, nous proposons des techniques pour produire des tests avec la détection des fautes temporelles et avec des transitions retardées et/ou instantanées. Afin d'évaluer l'applicabilité et l'efficacité de la méthode proposée, nous avons mis en œuvre deux outils: l’un en utilisant un simulateur industriel pour des modèles en LDS  et l’autre en employant un simulateur basé sur le langage IF. Deux  applications industrielles sont employées comme études de cas : Un système de Passage à Niveau et un Service Vocal fourni par France Telecom.

 Articles: