Les travaux présentés dans cette thèse se situent dans le cadre du domaine du test des systèmes réactifs. Nous avons appliqué la technique d'analyse de l'exécution symbolique pour le test de conformité et le test de raffinement. Les systèmes étudiés sont modélisés par des IOSTS. Pour vérifier la conformité entre une implantation et sa spécification d'origine, nous avons proposé un algorithme d'exécution symbolique de la spécification. Quatre verdicts sont émis : PASS, FAIL, INCONC et WeakPASS. Nous nous sommes aussi intéressés aux moyens pour vérifier qu'une spécification concrète raffine correctement une spécification abstraite. Nous avons proposé un algorithme de vérification qui sélectionne des traces observables à partir de la spécification abstraite et sont exécutées sur le système concret. Notre algorithme mène à un verdict statuant sur la correction de la relation de raffinement. / The work presented in this thesis are situated in testing reactives systems framework. We applied symbolic execution analysis technique for conformance testing and refinement testing. The studied systems are modelled by IOSTS. To check the conformance between an implemantation and its specification, we proposed an algorithm of generation of test case starting from test purposes extracted from the symbolic execution tree of the specification. Four verdicts are emitted~: PASS, FAIL, INCONC, and WeakPass. We were as interested in the means to check as a concrete specification refines an abstract specification and are executed on the concrete system. This selection is based on the techniques of symbolic execution. Our algorithm leads to a verdict to give a decision on the correction for the relation of refinement.
| Identifer | oai:union.ndltd.org:theses.fr/2006EVRY0029 |
| Date | 06 December 2006 |
| Creators | Touil, Assia |
| Contributors | Evry-Val d'Essonne, Le Gall, Pascale |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text, StillImage |
Page generated in 0.0022 seconds