Génération de séquences de tests de protocole à partir d'un réseau de Petri

Dans le cadre de ce mémoire, nous présenterons une approche basée sur l'analyse d'accessibilité pour dériver des séquences de tests à partir des spécifications décrites par des réseaux de Petri. Nous présenterons aussi un aperçu sur la validation des protocoles modélisés par les réseaux de Petri. Étant donné la complexité des protocoles de communication, la vérification et le test de la conformité d'une implantation par rapport à une spécification de référence sont d'une importance capitale. Dans ce contexte, plusieurs langages de description formelle peuvent être utilisés afin de rendre possibles cette vérification et ce test. Nous adoptons comme cadre de référence le concept de réseau de Petri qui est un modèle de spécification servant à la description du comportement d'un système. Par ailleurs, l'approche que nous avons appliquée dans notre travail consiste à vérifier la conformité d'une Implantation sous test (IST) à une spécification de référence, tout en dérivant, à partir de la spécification, des séquences de tests applicables à l'IST, afin d'observer la réaction de celle-ci acceptation ou blocage - vis-à-vis des séquences de tests. Cela permet de s'assurer que tous les comportements spécifiés sont correctement implantés