La phase la plus consommatrice de ressources d'une production de logiciels est l'étape de vérification qualité, incluant la vérification fonctionnelle des programmes. Donc, à cause de ces coûts, l'industrie de développement des logiciels exécute rarement une vérification minutieuse de ses produits. Une des stratégies les plus prometteuses pour réduire les coûts de vérification des logiciels est de rendre cette vérification aussi automatique que possible. Actuellement, cette industrie repose essentiellement sur une seule phase de tests pour vérifier les fonctionnalités des programmes. Nous avons donc cherché à automatiser le test fonctionnel des logiciels en fournissant une assistance pour l'étape de génération des scénarios de test. Le test basé sur des modèles (MBT) est une théorie de test qui a eu un grand succès dans l'automatisation du processus de test. Une méthode MBT analyse un modèle formel ou une spécification d'un logiciel pour produire des scénarios de test qui sont exécutés plus tard par le programme. La plupart de ces méthodes travaillent avec des machines à états finis (FSM) qui limite leur application puisque les FSMs ne peuvent pas décrire tous les logiciels. Cependant, un gros avantage de ces méthodes est qu'elles atteignent un haut degré d'automatisation. Dans cette thèse nous montrons, au contraire, le niveau d'automatisation que nous avons obtenu en appliquant une méthode MBT, connue comme Test Template Framework (TTF), sur des spécifications Z. Comme Z est basé sur la logique de premier ordre et la théorie du jeu, il est beaucoup plus expressif que les FSMs, rendant ainsi nos résultats applicables à une plus large gamme de programmes. / The most resource-consuming phase of software production is the verification of its qualities, including functional correctness. However, due to its costs, the software industry seldom performs a thorough verification of its products. One of the most promising strategies to reduce the costs of software verification is making it as automatic as possible. Currently, this industry relies basically only on testing to verify functional correctness. Therefore, we sought to automate functional testing of software systems by providing tool support for the test case generation step. Model-based testing (MBT) is a testing theory that has achieved impressive successes in automating the testing process. Any MBT method analyses a formal model or specification of the system under test to generate test cases that later are executed on the system. Almost all methods work with some form of finite state machines (FSM) which limits their application since FSM's cannot describe general systems. However, a great advantage of these methods is that they reach a high degree of automation. In this thesis we show, on the contrary, the degree of automation we have achieved by applying a MBT method, known as Test Template Framework (TTF), to Z specifications. Since Z is based on first-order logic and set theory it is far more expressive than FSM's, thus making our results applicable to a wider range of programs. During this thesis we have improved the TTF and developed a tool, called Fastest, that implements all of our ideas.

No description available.