• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 55
  • 19
  • 5
  • 5
  • 2
  • 2
  • 1
  • Tagged with
  • 90
  • 90
  • 90
  • 43
  • 40
  • 26
  • 26
  • 26
  • 23
  • 18
  • 17
  • 16
  • 14
  • 13
  • 12
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
81

Data-driven test automation : augmenting GUI testing in a web application

Kurin, Erik, Melin, Adam January 2013 (has links)
For many companies today, it is highly valuable to collect and analyse data in order to support decision making and functions of various sorts. However, this kind of data-driven approach is seldomly applied to software testing and there is often a lack of verification that the testing performed is relevant to how the system under test is used. Therefore, the aim of this thesis is to investigate the possibility of introducing a data-driven approach to test automation by extracting user behaviour data and curating it to form input for testing. A prestudy was initially conducted in order to collect and assess different data sources for augmenting the testing. After suitable data sources were identified, the required data, including data about user activity in the system, was extracted. This data was then processed and three prototypes where built on top of this data. The first prototype augments the model-based testing by automatically creating models of the most common user behaviour by utilising data mining algorithms. The second prototype tests the most frequent occurring client actions. The last prototype visualises which features of the system are not covered by automated regression testing. The data extracted and analysed in this thesis facilitates the understanding of the behaviour of the users in the system under test. The three prototypes implemented with this data as their foundation can be used to assist other testing methods by visualising test coverage and executing regression tests.
82

Détection de vulnérabilités appliquée à la vérification de code intermédiaire de Java Card / Vulnerability detection into Java Card bytecode verifier

Savary, Aymerick 30 June 2016 (has links)
La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n'étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG (Vulnerability Test Generation, génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d'intrusions est généré. Cette méthode s'inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d'application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L'extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d'une instruction. Cette méthode nous a permis de tester différents mécanismes d'implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d'étude, la méthode proposée est générique et a été appliquée à d'autres cas d'études. / Verification of the resistance of attacks against embedded implementations of the Java Card bytecode verifiers is a complex task. Current methods are not sufficient, only the generation of manual testing is possible. To automate this process, we propose a method called VTG (Vulnerability Test Generation). Based on a formal representation of the functional behavior of the system under test, a set of intrusion test is generated. This method is based on techniques of mutation and model-based testing. Initially, the model is transferred according to rules that we have defined to represent potential attacks. The tests are then extracted from the mutant models. Two Event-B models have been proposed. The first represents the structural constraints of the Java Card application files. The VTG allows in seconds to generate hundreds of abstract tests. The second model is composed of 66 events to represent 61 Java Card instructions. The mutation is effected in a few seconds. Extraction tests to generate 223 test 45 min. Each test checks a precondition or a combination of preconditions of a statement. This method allowed us to test different implementations of mechanisms through Java Card bytecode verifier. Although developed for our case study, the proposed method is generic and has been applied to other case studies.
83

Stratégies de génération de tests à partir de modèles UML/OCL interprétés en logique du premier ordre et système de contraintes. / Test generation strategies from UML/OCL models interpreted with first order logic constraints system

Cantenot, Jérôme 13 November 2013 (has links)
Les travaux présentés dans cette thèse proposent une méthode de génération automatique de tests à partir de modèles.Cette méthode emploie deux langages de modélisations UML4MBT et OCL4MBT qui ont été spécifiquement dérivées d’ UML et OCL pour la génération de tests. Ainsi les comportements, la structure et l’état initial du système sont décrits au travers des diagrammes de classes, d’objets et d’états-transitions.Pour générer des tests, l’évolution du modèle est représente sous la forme d’un système de transitions. Ainsi la construction de tests est équivalente à la découverte de séquences de transitions qui relient l’´état initial du système à des états validant les cibles de test.Ces séquences sont obtenues par la résolution de scénarios d’animations par des prouveurs SMT et solveurs CSP. Pour créer ces scénarios, des méta-modèles UML4MBT et CSP4MBT regroupant formules logiques et notions liées aux tests ont été établies pour chacun des outils.Afin d’optimiser les temps de générations, des stratégies ont été développé pour sélectionner et hiérarchiser les scénarios à résoudre. Ces stratégies s’appuient sur la parallélisation, les propriétés des solveurs et des prouveurs et les caractéristiques de nos encodages pour optimiser les performances. 5 stratégies emploient uniquement un prouveur et 2 stratégies reposent sur une collaboration du prouveur avec un solveur.Finalement l’intérêt de cette nouvelle méthode à été validée sur des cas d’études grâce à l’implémentation réalisée. / This thesis describes an automatic test generation process from models.This process uses two modelling languages, UML4MBT and OCL4MBT, created specificallyfor tests generation. Theses languages are derived from UML and OCL. Therefore the behaviours,the structure and the initial state of the system are described by the class diagram, the objectdiagram and the state-chart.To generate tests, the evolution of the model is encoded with a transition system. Consequently,to construct a test is to find transition sequences that rely the initial state of the system to thestates described by the test targets.The sequence are obtained by the resolution of animation scenarios. This resolution is executedby SMT provers and CSP solvers. To create the scenario, two dedicated meta-models, UML4MBTand CSP4MBT have been established. Theses meta-models associate first order logic formulas withthe test notions.7 strategies have been developed to improve the tests generation time. A strategy is responsiblefor the selection and the prioritization of the scenarios. A strategy is built upon the properties ofthe solvers and provers and the specification of our encoding process. Moreover the process canalso be paralleled to get better performance. 5 strategies employ only a prover and 2 make theprover collaborate with a solver.Finally the interest of this process has been evaluated through a list of benchmark on variouscases studies.
84

Aplicação de modelos de defeitos na geração de conjuntos de teste completos a partir de Sistemas de Transição com Entrada/Saída / Applying fault models in complete test suite generation from Input/Output Transition Systems

Sofia Larissa da Costa Paiva 16 March 2016 (has links)
O Teste Baseado em Modelos (TBM) emergiu como uma estratégia promissora para minimizar problemas relacionados à falta de tempo e recursos em teste de software e visa verificar se a implementação sob teste está em conformidade com sua especificação. Casos de teste são gerados automaticamente a partir de modelos comportamentais produzidos durante o ciclo de desenvolvimento de software. Entre as técnicas de modelagem existentes, Sistemas de Transição com Entrada/Saída (do inglês, Input/Output Transition Systems - IOTSs), são modelos amplamente utilizados no TBM por serem mais expressivos do que Máquinas de Estado Finito (MEFs). Apesar dos métodos existentes para geração de testes a partir de IOTSs, o problema da seleção de casos de testes é um tópico difícil e importante. Os métodos existentes para IOTS são não-determinísticos, ao contrário da teoria existente para MEFs, que fornece garantia de cobertura completa com base em um modelo de defeitos. Esta tese investiga a aplicação de modelos de defeitos em métodos determinísticos de geração de testes a partir de IOTSs. Foi proposto um método para geração de conjuntos de teste com base no método W para MEFs. O método gera conjuntos de teste de forma determinística além de satisfazer condições de suficiência de cobertura da especificação e de todos os defeitos do domínio de defeitos definido. Estudos empíricos avaliaram a aplicabilidade e eficácia do método proposto: resultados experimentais para analisar o custo de geração de conjuntos de teste utilizando IOTSs gerados aleatoriamente e um estudo de caso com especificações da indústria mostram a efetividade dos conjuntos gerados em relação ao método tradicional de Tretmans. / Model-Based Testing (MBT) has emerged as a promising strategy for the minimization of problems related to time and resource limitations in software testing and aims at checking whether the implementation under test is in compliance with its specification. Test cases are automatically generated from behavioral models produced during the software development life cycle. Among the existing modeling techniques, Input/Output Transition Systems (IOTSs) have been widely used in MBT because they are more expressive than Finite State Machines (FSMs). Despite the existence of test generation methods for IOTSs, the problem of selection of test cases is an important and difficult topic. The current methods for IOTSs are non-deterministic, in contrast to the existing theory for FSMs that provides complete fault coverage guarantee based on a fault model. This manuscript addresses the application of fault models to deterministic test generation methods from IOTSs. A method for the test suite generation based on W method for FSMs is proposed for IOTSs. It generates test suites in a deterministic way and also satisfies sufficient conditions of specification coverage and all faults in a given fault domain. Empirical studies evaluated its applicability and effectiveness. Experimental results for the analyses of the cost of test suite generation by random IOTSs and a case study with specifications from the industry show the effectiveness of the test suites generated in relation to the traditional method of Tretmans.
85

Testing Self-Adaptive Systems

Püschel, Georg 14 September 2018 (has links)
Autonomy is the most demanded yet hard-to-achieve feature of recent and future software systems. Self-driving cars, mail-delivering drones, automated guided vehicles in production sites, and housekeeping robots need to decide autonomously during most of their operation time. As soon as human intervention becomes necessary, the cost of ownership increases, and this must be avoided. Although the algorithms controlling autonomous systems become more and more intelligent, their hardest opponent is their inflexibility. The more environmental situations such a system is confronted with, the more complexity the control of the autonomous system will have to master. To cope with this challenge, engineers have approached a system design, which adopts feedback loops from nature. The resulting architectural principle, which they call self-adaptive systems, follows the idea of iteratively gathering sensor data, analyzing it, planning new adaptations of the system, and finally executing the plan. Often, adaptation means to alter the system setup, re-wire components, or even exchange control algorithms to keep meeting goals and requirements in the newly appeared situation. Although self-adaptivity helps engineers to organize the vast amount of information in a self-deciding system, it remains hard to deal with the variety of contexts, which involve both environmental influences and knowledge about the system\'s internals. This challenge not only holds for the construction phase but also for verification and validation, including software test. To assure sufficient quality of a system, it must be tested under an enormous and, thus, unmanageable, number of different contextual situations and manual test-cases. This thesis proposes a novel set of methods and model types, which help test engineers to specify precisely what they expect from a self-adaptive system under test. The formal nature of the introduced artifacts allows for automatically generating test-suites or running simulations in the loop so that a qualitative verdict on the system\'s correctness can be gained. Additional to these conceptional contributions, the thesis describes a model-based adaptivity test environment, which test engineers can use for testing actual self-adaptive systems. The implementation includes comprehensive tooling for creating the introduced types of models, generating test-cases, simulating them in the loop, automating tests, and reporting. Composing all enabling components for these tasks constitutes a reference architecture of integrated test environments for self-adaptive systems. We demonstrate the completeness and accuracy of the technical approach together with the underlying concepts by evaluating them in an experimental case study where an autonomous robot interacts with human co-workers. In summary, this thesis proposes concepts for automatically and, thus, efficiently testing self-adaptive systems. The quality, which is fostered by this novel approach, is resilience: the ability of a system to maintain its promises while facing changing environments.:1 Introduction 1 1.1 Problem Description 1 1.2 Overview of Adopted Methods 3 1.3 Hypothesis and Main Contributions 4 1.4 Organization of This Thesis 5 I Foundations 7 2 Background 9 2.1 Self-adaptive Software and Autonomic Computing 9 2.1.1 Common Principles and Components of SAS 10 2.1.2 Concrete Implementations and Applications of SAS 12 2.2 Model-based Testing 13 2.2.1 Testing for Dependability 14 2.2.2 The Basics of Testing 15 2.2.3 Automated Test Design 18 2.3 Dynamic Variability Management 22 2.3.1 Software Product Lines 23 2.3.2 Dynamic Software Product Lines 25 3 Related Work: Existing Research on Testing Self-Adaptive Systems 29 3.1 Testing Context-Aware Applications 30 3.2 The SimSOTA Project 31 3.3 Dynamic Variability in Complex Adaptive Systems (DiVA) 33 3.4 Other Early-Stage Research 34 3.5 Taxonomy of Requirements of Model-based SAS Testing 36 II Methods 39 4 Model-driven SAS Testing 41 4.1 Problem/Solution Fit 41 4.2 Example: Surveillance Drone 43 4.3 Concepts and Models for Testing Self-Adaptive Systems 44 4.3.1 Test Case Generation vs. Simulation in the Loop 44 4.3.2 Incremental Modeling Process 45 4.3.3 Basic Representation Format: Petri Nets 46 4.3.4 Context Variation 50 4.3.5 Modeling Adaptive Behavior 53 4.3.6 Dynamic Context Change 57 4.3.7 Interfacing Context from Behavioral Representation 62 4.3.8 Adaptation Mode Variation 64 4.3.9 Context-Dependent Recon guration 67 4.4 Adequacy Criteria for SAS Test Models 71 4.5 Discussion on the Viability of the Employed Models 71 4.6 Comparison to Related Work 73 4.7 Summary and Discussion 74 5 Model-based Adaptivity Test Environment 75 5.1 Technological Foundation 76 5.2 MATE Base Components 77 5.3 Metamodel Implementation 78 5.3.1 Feature-based Variability Model 79 5.3.2 Abstract and Concrete Syntax for Textual Notations 80 5.3.3 Adaptive Petri Nets 86 5.3.4 Stimulus and Recon guration Automata 87 5.3.5 Test Suite and Report Model 87 5.4 Test Generation Framework 87 5.5 Test Automation Framework 91 5.6 MATE Tooling and the SAS Test Process 93 5.6.1 Test Modeling 94 5.6.2 Test Case Generation 95 5.6.3 Test Case Execution and Test Reporting 96 5.6.4 Interactive Simulation Frontend 96 5.7 Summary and Discussion 97 III Evaluation 99 6 Experimental Study: Self-Adaptive Co-Working Robots 101 6.1 Robot Teaching and Co-Working with WEIR 103 6.1.1 WEIR Hardware Components 104 6.1.2 WEIR Software Infrastructure 105 6.1.3 KUKA LBR iiwa as WEIR Manipulator 106 6.1.4 Self-Adaptation Capabilities of WEIR 107 6.2 Cinderella as Testable Co-Working Application 109 6.2.1 Cinderella Setup and Basic Functionality 109 6.2.2 Co-Working with Cinderella 110 6.3 Testing Cinderella with MATE 112 6.3.1 Automating Test Execution 112 6.3.2 Modeling Cinderella in MATE 113 6.3.3 Testing Cinderella in the Loop 121 6.4 Evaluation Verdict and Summary 123 7 Summary and Discussion 125 7.1 Summary of Contributions 126 7.2 Open Research Questions 127 Bibliography 129 Appendices 137 Appendix Cinderella De nitions 139 1 Cinderella Adaptation Bounds 139 2 Cinderella Self-adaptive Workflow 140
86

Learning Finite State Machine Specifications from Test Cases / Lernen von Spezifikationen in Form von endlichen Zustandsmaschinen aus Testfällen

Werner, Edith Benedicta Maria 01 June 2010 (has links)
No description available.
87

NAT2TEST: generating test cases from natural language requirements based on CSP

CARVALHO, Gustavo Henrique Porto de 26 February 2016 (has links)
Submitted by Natalia de Souza Gonçalves (natalia.goncalves@ufpe.br) on 2016-09-28T12:33:15Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) GustavoHPCarvalho_Doutorado_CInUFPE_2016.pdf: 1763137 bytes, checksum: aed7b3ab2f6235757818003678633c9b (MD5) / Made available in DSpace on 2016-09-28T12:33:15Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) GustavoHPCarvalho_Doutorado_CInUFPE_2016.pdf: 1763137 bytes, checksum: aed7b3ab2f6235757818003678633c9b (MD5) Previous issue date: 2016-02-26 / High trustworthiness levels are usually required when developing critical systems, and model based testing (MBT) techniques play an important role generating test cases from specification models. Concerning critical systems, these models are usually created using formal or semi-formal notations. Moreover, it is also desired to clearly and formally state the conditions necessary to guarantee that an implementation is correct with respect to its specification by means of a conformance relation, which can be used to prove that the test generation strategy is sound. Despite the benefits of MBT, those who are not familiar with the models syntax and semantics may be reluctant to adopt these formalisms. Furthermore, most of these models are not available in the very beginning of the project, when usually natural-language requirements are available. Therefore, the use of MBT is postponed. Here, we propose an MBT strategy for generating test cases from controlled naturallanguage (CNL) requirements: NAT2TEST, which refrains the user from knowing the syntax and semantics of the underlying notations, besides allowing early use of MBT via naturallanguage processing techniques; the formal and semi-formal models internally used by our strategy are automatically generated from the natural-language requirements. Our approach is tailored to data-flow reactive systems: a class of embedded systems whose inputs and outputs are always available as signals. These systems can also have timed-based behaviour, which may be discrete or continuous. The NAT2TEST strategy comprises a number of phases. Initially, the requirements are syntactically analysed according to a CNL we proposed to describe data-flow reactive systems. Then, the requirements informal semantics are characterised based on the case grammar theory. Afterwards, we derive a formal representation of the requirements considering a model of dataflow reactive systems we defined. Finally, this formal model is translated into communicating sequential processes (CSP) to provide means for generating test cases. We prove that our test generation strategy is sound with respect to our timed input-output conformance relation based on CSP: csptio. Besides CSP, we explore the generation of other target notations (SCR and IMR) from which we can generate test cases using commercial tools (T-VEC and RT-Tester, respectively). The whole process is fully automated by the NAT2TEST tool. Our strategy was evaluated considering examples from the literature, the aerospace (Embraer) and the automotive (Mercedes) industry. We analysed performance and the ability to detect defects generated via mutation. In general, our strategy outperformed the considered baseline: random testing. We also compared our strategy with relevant commercial tools. / Testes baseados em modelos (MBT) consiste em criar modelos para especificar o comportamento esperado de sistemas e, a partir destes, gerar testes que verificam se implementações possuem o nível de confiabilidade esperado. No contexto de sistemas críticos, estes modelos são normalmente (semi)formais e deseja-se uma definição precisa das condições necessárias para garantir que uma implementação é correta em relação ao modelo da especificação. Esta definição caracteriza uma relação de conformidade, que pode ser usada para provar que uma estratégia de MBT é consistente (sound). Apesar dos benefícios, aqueles sem familiaridade com a sintaxe e a semântica dos modelos empregados podem relutar em adotar estes formalismos. Aqui, propõe-se uma estratégia de MBT para gerar casos de teste a partir de linguagem natural controlada (CNL). Esta estratégia (NAT2TEST) dispensa a necessidade de conhecer a sintaxe e a semântica das notações formais utilizadas internamente, uma vez que os modelos intermediários são gerados automaticamente a partir de requisitos em linguagem natural. Esta estratégia é apropriada para sistemas reativos baseados em fluxos de dados: uma classe de sistemas embarcados cujas entradas e saídas estão sempre disponíveis como sinais. Estes sistemas também podem ter comportamento dependente do tempo (discreto ou contínuo). Na estratégia NAT2TEST, inicialmente, os requisitos são analisados sintaticamente de acordo com a CNL proposta neste trabalho para descrever sistemas reativos. Em seguida, a semântica informal dos requisitos é caracterizada utilizando a teoria de gramática de casos. Posteriormente, deriva-se uma representação formal dos requisitos considerando um modelo definido neste trabalho para sistemas reativos. Finalmente, este modelo é traduzido em uma especificação em communicating sequential processes (CSP) para permitir a geração de testes. Este trabalho prova que a estratégia de testes proposta é consistente considerando a relação de conformidade temporal baseada em entradas e saídas também definida aqui: csptio. Além de CSP, foi explorada a geração de outras notações formais (SCR e IMR), a partir das quais é possível gerar casos de teste usando ferramentas comerciais (T-VEC e RT-Tester, respectivamente). Todo o processo é automatizado pela ferramenta NAT2TEST. A estratégia NAT2TEST foi avaliada considerando exemplos da literatura, da indústria aeroespacial (Embraer) e da automotiva (Mercedes). Foram analisados o desempenho e a capacidade de detectar defeitos gerados através de operadores de mutação. Em geral, a estratégia NAT2TEST apresentou melhores resultados do que a referência adotada: testes aleatórios. A estratégia NAT2TEST também foi comparada com ferramentas comerciais relevantes.
88

A pattern-driven and model-based vulnerability testing for Web applications / Une approche à base de modèles et de patterns pour le test de vulnérabilités d'applications Web

Vernotte, Alexandre 29 October 2015 (has links)
Cette thèse propose une approche originale de test de vulnérabilité Web à partir de modèles etdirigée par des patterns de tests, nommée PMVT. Son objectif est d’améliorer la capacité de détectionde quatre types de vulnérabilité majeurs, Cross-Site Scripting, Injections SQL, Cross-Site RequestForgery, et Privilege Escalation. PMVT repose sur l’utilisation d’un modèle comportemental del’application Web, capturant ses aspects fonctionnels, et sur un ensemble de patterns de test devulnérabilité qui adressent un type de vulnérabilité de manière générique, quelque soit le type del’application Web sous test.Par l’adaptation de technologies MBT existantes, nous avons développé une chaîne outillée complèteautomatisant la détection des quatre types de vulnérabilité. Ce prototype a été exprimenté et évaluésur deux applications réelles, actuellement utiliseés par plusieurs dizaines de milliers d’utilisateurs.Les résultats d’expérimentation démontrent la pertinence et de l’efficience de PMVT, notamment enaméliorant de façon significative la capacité de détection de vulnérabilités vis à vis des scannersautomatiques d’applications Web existants. / This thesis proposes an original approach, dubbed PMVT for Pattern-driven and Model-basedVulnerability Testing, which aims to improve the capability for detecting four high-profile vulnerabilitytypes, Cross-Site Scripting, SQL Injections, CSRF and Privilege Escalations, and reduce falsepositives and false negatives verdicts. PMVT relies on the use of a behavioral model of theapplication, capturing its functional aspects, and a set of vulnerability test patterns that addressvulnerabilities in a generic way. By adapting existing MBT technologies, an integrated toolchain that supports PMVT automates thedetection of the four vulnerability types in Web applications. This prototype has been experimentedand evaluated on two real-life Web applications that are currently used by tens of thousandsusers. Experiments have highlighted the effectiveness and efficiency of PMVT and shown astrong improvement of vulnerability detection capabilities w.r.t. available automated Web applicationscanners for these kind of vulnerabilities.
89

Automatické generování testů pro GNOME GUI aplikace z metadat AT-SPI / Automated Generation of Tests for GNOME GUI Applications Using AT-SPI Metadata

Krajňák, Martin January 2020 (has links)
Cieľom tejto práce je vývoj nástroja na automatické generovanie testov pre aplikácie s grafickým užívateľským rozhraním v~prostredí GNOME. Na generovanie testov sú použité metadáta asistenčných technológií, konrétne AT-SPI. Navrhnutý generátor testov využíva dané metadáta na vytvorenie modelu testovanej aplikácie. Model mapuje sekvencie udalostí, ktoré generátor vykoná na testovanej aplikácii počas generovania testov. Súčasťou procesu generovania je zároveň detekcia závažných chýb v testovaných aplikáciách. Výstupom procesu generovania sú automatizované testy, ktoré sú vhodné na regresné testovanie. Funkčnosť implementovaného generátora testov bola úspešne overená testovaním 5 aplikácií s otvoreným zdrojovým kódom. Počas testovania aplikácií navrhnutým nástrojom sa preukázala schopnosť detekovať nové chyby.
90

Model-Based Testing of Timed Distributed Systems : A Constraint-Based Approach for Solving the Oracle Problem / Test à base de modèles de systèmes temporisés distribués : une approche basée sur les contraintes pour résoudre le problème de l’oracle

Benharrat, Nassim 14 February 2018 (has links)
Le test à base de modèles des systèmes réactifs est le processus de vérifier si un système sous test (SUT) est conforme à sa spécification. Il consiste à gérer à la fois la génération des données de test et le calcul de verdicts en utilisant des modèles. Nous spécifions le comportement des systèmes réactifs à l'aide des systèmes de transitions symboliques temporisées à entrée-sortie (TIOSTS). Quand les TIOSTSs sont utilisés pour tester des systèmes avec une interface centralisée, l'utilisateur peut ordonner complètement les événements (i.e., les entrées envoyées au système et les sorties produites). Les interactions entre le testeur et le SUT consistent en des séquences d'entrées et de sortie nommées traces, pouvant être séparées par des durées dans le cadre du test temporisé, pour former ce que l'on appelle des traces temporisées. Les systèmes distribués sont des collections de composants locaux communiquant entre eux et interagissant avec leur environnement via des interfaces physiquement distribuées. Différents événements survenant à ces différentes interfaces ne peuvent plus être ordonnés. Cette thèse concerne le test de conformité des systèmes distribués où un testeur est placé à chaque interface localisée et peut observer ce qui se passe à cette interface. Nous supposons qu'il n'y a pas d’horloge commune mais seulement des horloges locales pour chaque interface. La sémantique de tels systèmes est définie comme des tuples de traces temporisées. Nous considérons une approche du test dans le contexte de la relation de conformité distribuée dtioco. La conformité globale peut être testée dans une architecture de test en utilisant des testeurs locaux sans communication entre eux. Nous proposons un algorithme pour vérifier la communication pour un tuple de traces temporisées en formulant le problème de message-passing en un problème de satisfaction de contraintes (CSP). Nous avons mis en œuvre le calcul des verdicts de test en orchestrant à la fois les algorithmes du test centralisé off-line de chacun des composants et la vérification des communications par le biais d'un solveur de contraintes. Nous avons validé notre approche sur un cas étude de taille significative. / Model-based testing of reactive systems is the process of checking if a System Under Test (SUT) conforms to its model. It consists of handling both test data generation and verdict computation by using models. We specify the behaviour of reactive systems using Timed Input Output Symbolic Transition Systems (TIOSTS) that are timed automata enriched with symbolic mechanisms to handle data. When TIOSTSs are used to test systems with a centralized interface, the user may completely order events occurring at this interface (i.e., inputs sent to the system and outputs produced from it). Interactions between the tester and the SUT are sequences of inputs and outputs named traces, separated by delays in the timed framework, to form so-called timed traces. Distributed systems are collections of communicating local components which interact with their environment at physically distributed interfaces. Interacting with such a distributed system requires exchanging values with it by means of several interfaces in the same testing process. Different events occurring at different interfaces cannot be ordered any more. This thesis focuses on conformance testing for distributed systems where a separate tester is placed at each localized interface and may only observe what happens at this interface. We assume that there is no global clock but only local clocks for each localized interface. The semantics of such systems can be seen as tuples of timed traces. We consider a framework for distributed testing from TIOSTS along with corresponding test hypotheses and a distributed conformance relation called dtioco. Global conformance can be tested in a distributed testing architecture using only local testers without any communication between them. We propose an algorithm to check communication policy for a tuple of timed traces by formulating the verification of message passing in terms of Constraint Satisfaction Problem (CSP). Hence, we were able to implement the computation of test verdicts by orchestrating both localised off-line testing algorithms and the verification of constraints defined by message passing that can be supported by a constraint solver. Lastly, we validated our approach on a real case study of a telecommunications distributed system.

Page generated in 0.054 seconds