• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 25
  • 9
  • 8
  • 5
  • 4
  • 1
  • 1
  • Tagged with
  • 65
  • 65
  • 27
  • 16
  • 15
  • 15
  • 14
  • 13
  • 12
  • 11
  • 10
  • 10
  • 10
  • 9
  • 8
  • 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.
51

Test generation and animation based on object-oriented specifications / Génération de tests et animation à partir de spécifications orientées objet

Krieger, Matthias 09 December 2011 (has links)
L'objectif de cette thèse est l'assistance à la génération de tests et à l'animation de spécifications orientées objet. Nous cherchons en particulier à profiter de l'état de l'art des techniques de résolution de satisfaisabilité en utilisant une représentation appropriée des données orientées objet. Alors que la génération automatique de cas de tests recherche un large ensemble de valeurs à fournir en entrée d'une application, l’animation de spécifications effectue les calculs qui sont conformes à une spécification à partir de valeurs fournies par l'utilisateur. L'animation est une technique importante pour la validation des spécifications.Comme fondement de ce travail, nous présentons des clarifications et une formalisation partielle du langage de spécification OCL (Object Constraint Language) ainsi que quelques extensions, afin de permettre la génération de tests et l'animation à partir de spécifications OCL.Pour la génération de tests, nous avons implémenté plusieurs améliorations à HOL-TestGen, outil basé sur le démonstrateur de théorème Isabelle, qui engendre des tests à partir de spécifications en Logique d’Ordre Supérieure (Higher-Order Logic ou HOL). Nous montrons comment des solveurs SMT peuvent être utilisés pour résoudre différents types de contraintes en HOL et nous présentons une approche modulaire de raisonnement par cas pour dériver des cas de tests. Cette dernière approche facilite l'introduction de règles de decomposition par cas qui sont adaptées aux spécifications orientées objet.Pour l'animation de spécifications, nous avons développé OCLexec, outil d'animation de spécifications en OCL. A partir de contrats de fonctions OCLexec produit les implémentations Java correspondantes qui appellent un solveur de contraintes SMT lors de leur exécution. / The goal of this thesis is the development of support for test generation and animation based on object-oriented specifications. We aim particularly to take advantage of state-of-the-art satisfiability solving techniques by using an appropriate representation of object-oriented data. While automated test generation seeks a large set of data to execute an implementation on, animation performs computations that comply with a specification based on user-provided input data. Animation is a valuable technique for validating specifications.As a foundation of this work, we present clarifications and a partial formalization of the Object Constraint Language (OCL) as well as some extensions in order to allow for test generation and animation based on OCL specifications.For test generation, we have implemented several enhancements to HOL-TestGen, a tool built on top of the Isabelle theorem proving system that generates tests from specifications in Higher-Order Logic (HOL). We show how SMT solvers can be used to solve various types of constraints in HOL and present a modular approach to case splitting for deriving test cases. The latter facilitates the introduction of splitting rules that are tailored to object-oriented specifications.For animation, we implemented the tool OCLexec for animating OCL specifications. OCLexec generates from operation contracts corresponding Java implementations that call an SMT-based constraint solver at runtime.
52

Formal methods for functional verification of cache-coherent systems-on-chip / Méthodes Formelles pour la vérification fonctionnelle des systèmes sur puce cache cohérent

Kriouile, Abderahman 17 September 2015 (has links)
Les architectures des systèmes sur puce (System-on-Chip, SoC) actuelles intègrent de nombreux composants différents tels que les processeurs, les accélérateurs, les mémoires et les blocs d'entrée/sortie, certains pouvant contenir des caches. Vu que l'effort de validation basée sur la simulation, actuellement utilisée dans l'industrie, croît de façon exponentielle avec la complexité des SoCs, nous nous intéressons à des techniques de vérification formelle. Nous utilisons la boîte à outils CADP pour développer et valider un modèle formel d'un SoC générique conforme à la spécification AMBA 4 ACE récemment proposée par ARM dans le but de mettre en œuvre la cohérence de cache au niveau système. Nous utilisons une spécification orientée contraintes pour modéliser les exigences générales de cette spécification. Les propriétés du système sont vérifié à la fois sur le modèle avec contraintes et le modèle sans contraintes pour détecter les cas intéressants pour la cohérence de cache. La paramétrisation du modèle proposé a permis de produire l'ensemble complet des contre-exemples qui ne satisfont pas une certaine propriété dans le modèle non contraint. Notre approche améliore les techniques industrielles de vérification basées sur la simulation en deux aspects. D'une part, nous suggérons l'utilisation du modèle formel pour évaluer la bonne construction d'une unité de vérification d'interface. D'autre part, dans l'objectif de générer des cas de test semi-dirigés intelligents à partir des propriétés de logique temporelle, nous proposons une approche en deux étapes. La première étape consiste à générer des cas de tests abstraits au niveau système en utilisant des outils de test basé sur modèle de la boîte à outils CADP. La seconde étape consiste à affiner ces tests en cas de tests concrets au niveau de l'interface qui peuvent être exécutés en RTL grâce aux services d'un outil commercial de génération de tests dirigés par les mesures de couverture. Nous avons constaté que notre approche participe dans la transition entre la vérification du niveau interface, classiquement pratiquée dans l'industrie du matériel, et la vérification au niveau système. Notre approche facilite aussi la validation des propriétés globales du système, et permet une détection précoce des bugs, tant dans le SoC que dans les bancs de test commerciales. / State-of-the-art System-on-Chip (SoC) architectures integrate many different components, such as processors, accelerators, memories, and I/O blocks. Some of those components, but not all, may have caches. Because the effort of validation with simulation-based techniques, currently used in industry, grows exponentially with the complexity of the SoC, this thesis investigates the use of formal verification techniques in this context. More precisely, we use the CADP toolbox to develop and validate a generic formal model of a heterogeneous cache-coherent SoC compliant with the recent AMBA 4 ACE specification proposed by ARM. We use a constraint-oriented specification style to model the general requirements of the specification. We verify system properties on both the constrained and unconstrained model to detect the cache coherency corner cases. We take advantage of the parametrization of the proposed model to produce a comprehensive set of counterexamples of non-satisfied properties in the unconstrained model. The results of formal verification are then used to improve the industrial simulation-based verification techniques in two aspects. On the one hand, we suggest using the formal model to assess the sanity of an interface verification unit. On the other hand, in order to generate clever semi-directed test cases from temporal logic properties, we propose a two-step approach. One step consists in generating system-level abstract test cases using model-based testing tools of the CADP toolbox. The other step consists in refining those tests into interface-level concrete test cases that can be executed at RTL level with a commercial Coverage-Directed Test Generation tool. We found that our approach helps in the transition between interface-level and system-level verification, facilitates the validation of system-level properties, and enables early detection of bugs in both the SoC and the commercial test-bench.
53

Recherche de vulnérabilités logicielles par combinaison d'analyses de code binaire et de frelatage (Fuzzing) / Software vulnerability research combining fuzz testing and binary code analysis

Bekrar, Sofia 10 October 2013 (has links)
Le frelatage (ou fuzzing) est l'une des approches les plus efficaces pour la détection de vulnérabilités dans les logiciels de tailles importantes et dont le code source n'est pas disponible. Malgré une utilisation très répandue dans l'industrie, les techniques de frelatage "classique" peuvent avoir des résultats assez limités, et pas toujours probants. Ceci est dû notamment à une faible couverture des programmes testés, ce qui entraîne une augmentation du nombre de faux-négatifs; et un manque de connaissances sur le fonctionnement interne de la cible, ce qui limite la qualité des entrées générées. Nous présentons dans ce travail une approche automatique de recherche de vulnérabilités logicielles par des processus de test combinant analyses avancées de code binaire et frelatage. Cette approche comprend : une technique de minimisation de suite de tests, pour optimiser le rapport entre la quantité de code testé et le temps d'exécution ; une technique d'analyse de couverture optimisée et rapide, pour évaluer l'efficacité du frelatage ; une technique d'analyse statique, pour localiser les séquences de codes potentiellement sensibles par rapport à des patrons de vulnérabilités; une technique dynamique d'analyse de teinte, pour identifier avec précision les zones de l'entrée qui peuvent être à l'origine de déclenchements de vulnérabilités; et finalement une technique évolutionniste de génération de test qui s'appuie sur les résultats des autres analyses, afin d'affiner les critères de décision et d'améliorer la qualité des entrées produites. Cette approche a été mise en œuvre à travers une chaîne d'outils intégrés et évalués sur de nombreuses études de cas fournies par l'entreprise. Les résultats obtenus montrent son efficacité dans la détection automatique de vulnérabilités affectant des applications majeures et sans accès au code source. / Fuzz testing (a.k.a. fuzzing) is one of the most effective approaches for discovering security vulnerabilities in large and closed-source software. Despite their wide use in the software industry, traditional fuzzing techniques suffer from a poor coverage, which results in a large number of false negatives. The other common drawback is the lack of knowledge about the application internals. This limits their ability to generate high quality inputs. Thus such techniques have limited fault detection capabilities. We present an automated smart fuzzing approach which combines advanced binary code analysis techniques. Our approach has five components. A test suite reduction technique, to optimize the ratio between the amount of covered code and the execution time. A fast and optimized code coverage measurement technique, to evaluate the fuzzing effectiveness. A static analysis technique, to locate potentially sensitive sequences of code with respect to vulnerability patterns. An origin-aware dynamic taint analysis technique, to precisely identify the input fields that may trigger potential vulnerabilities. Finally, an evolutionary based test generation technique, to produce relevant inputs. We implemented our approach as an integrated tool chain, and we evaluated it on numerous industrial case studies. The obtained results demonstrate its effectiveness in automatically discovering zero-day vulnerabilities in major closed-source applications. Our approach is relevant to both defensive and offensive security purposes.
54

A black-box testing technique for the detection of crashes based on automated test scenarios

PERES, Glaucia Boudox 31 January 2009 (has links)
Made available in DSpace on 2014-06-12T15:57:23Z (GMT). No. of bitstreams: 2 arquivo3187_1.pdf: 2434276 bytes, checksum: df6b126c4802eed8524aba0d3cb25af9 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Boudox Peres, Glaucia; Cabral Mota, Alexandre. A black-box testing technique for the detection of crashes based on automated test scenarios. 2009. Dissertação (Mestrado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2009.
55

Evidências sobre o uso de técnicas de geração automática de dados de teste em programas concorrentes / Evidences about the use of automatic test data generation techniques in context of concurrent programs

Ricardo Ferreira Vilela 01 August 2016 (has links)
Diversas pesquisas apoiam e investigam o teste de programas concorrentes, as quais objetivam, principalmente, a proposição de critérios de teste e mecanismos para execução das diferentes sincronizações entre processos ou threads. As características específicas dessas aplicações podem ocasionar diferentes tipos de defeitos, os quais, em sua maioria, não são facilmente identificados. Nesse contexto, a geração automática de dados de teste pode apoiar a atividade de teste atuando na seleção de entradas mais representativas, ou seja, aquelas com maior probabilidade de revelar defeitos. Apesar disso, poucas pesquisas abordam este tema no contexto de programas concorrentes, e as existentes não consideram aspectos importantes desse tipo de aplicação. A geração de dados de teste para programas sequenciais dispõe de uma variedade de técnicas que apoiam a seleção dos dados de teste. Essas técnicas têm sido estendidas para o contexto de programas concorrentes partindo da premissa que esses programas necessitam de abordagens mais complexas para seleção de entradas, em decorrência disso um maior custo é imposto ao teste. Considerando esse contexto, uma lacuna ainda em aberto é a avaliação das técnicas para o cenário de programas concorrentes. Neste trabalho a avaliação das técnicas foi explorada por meio da realização de estudos experimentais, os quais avaliaram diferentes técnicas de geração de dados de teste para o contexto de programas concorrentes, considerando a eficácia em revelar defeitos, cobertura de critérios e custo para atividade de teste. Os resultados obtidos demonstraram que as técnicas empregadas para programas sequenciais não atingem o mínimo esperado para este tipo aplicação. Apesar disso, as técnicas investigadas apresentaram características importantes que podem auxiliar a atividade de teste para programas concorrentes e a proposição de abordagens efetivas de geração de dados para esse contexto. / The concurrent program testing has been largely investigated with propositions of testing criteria and mechanisms, which aim mainly to testing criteria proposition and mechanisms for execution of different synchronizations. The specific characteristics of these applications can lead to the different types of faults, which, in most of cases, are not easily identified. In this context, the automatic test data generation can support the testing activity acting in selecting the most representative data tests, i.e. those most likely to reveal faults. Nevertheless, few studies address this issue in the context of concurrent programs, and the these studies do not consider important aspects of this type of application. In contrast, we can find several techniques proposed to support the test data generation for sequential programs. These techniques have been extended to the context of concurrent programs on the premise that these programs require more complex approaches for selection of test data. As a result, a greater cost for testing activity is enforced. Considering this context, a gap still open is the evaluation of techniques for the scenario of concurrent programs. In this work the evaluation of techniques was explored through experimental studies, which different techniques of test data generatoon were evaluated, considering effectiveness, testing coverage and application cost. The results showed that the generation techniques used for sequential programs used in the experimental study do not reach the minimum expected in terms of effectiveness and cost for concurrent programs. Nevertheless, the techniques investigated showed significant features that can help the proposition of effective approaches for test data generation applied to concurrent programs.
56

Automatic generation of configurable test-suites for software product lines / Geração automática de conjuntos de teste configuráveis para linhas de produto de software

Fragal, Vanderson Hafemann 28 November 2017 (has links)
Software Product Line Engineering (SPLE) is an approach used in the development of similar products, which explores the systematic reuse of software artifacts. The SPLE process has several activities executed to ensure software quality. Quality assurance is of vital importance for achieving and maintaining a high quality of all kinds of artifacts, such as products and processes. Testing activities are widely used in the industry for quality management. However, the effort for applying testing is usually high, and increasing the testing efficiency is a major concern of all systems engineering activities. A common means of increasing efficiency is automation of the test execution and the test design. Automated test design can be performed using approaches such as Model-Based Testing (MBT) in which the real behavior of a software system is compared to an abstract test model. Several techniques, processes, and strategies were developed for SPLE testing, but still many problems are open in this area of research. The challenge in focus is the reduction of the overall test effort required to test SPLE products. Test effort can be reduced by maximizing test reuse using models that take advantage of the similarity between products. The thesis goal is to automate the generation of small test-suites with high fault detection and low test redundancy between products. To achieve the goal, equivalent tests are identified for a set of products using complete and configurable test-suites. Two research directions are explored, one is product-based centered, and the other is product line-centered. For test design, test-suites that have full fault coverage were generated from state machines with and without feature constraints. A prototype implementation tool was developed for test design automation. In addition, the proposed approach was evaluated using examples, experimental studies, and an industrial case study for the automotive domain. The results indicates test effort reduction of 36% in the first research direction for a product line with 24 products, and in the second research direction increasing test effort reduction based on the number of products that require testing. For 6 products 15% reduction (from case study), and for 20 random products 50% reduction (from experimental studies). / Engenharia de Linha de Produto de Software (SPLE) é uma abordagem utilizada no desenvolvimento de produtos similares, que explora a reutilização sistemática de artefatos de software. O processo da SPLE executa várias atividades para garantir a qualidade do software. Atividades de garantia de qualidade são fundamentais para alcançar e manter altos níveis de qualidade em todos os tipos de artefatos de software, tais como produtos e processos. Atividades de teste são amplamente utilizadas na indústria para o gerenciamento de qualidade. No entanto, o esforço para a aplicação de testes geralmente é alto e melhorar a eficiência dos testes é um desafio relacionado a todas as atividades da engenharia de sistemas. Uma maneira de melhorar a eficiência da atividade de teste é automatizar a geração e execução dos testes. A geração automática de testes pode ser realizada por abordagens tais como o Teste Baseado em Modelos (TBM), em que o comportamento real do sistema de software é comparado a um modelo de teste abstrato. Várias técnicas, processos e estratégias foram desenvolvidas para o teste de SPLE, contudo, existem diversos desafios nessa área de pesquisa. O desafio em foco é a redução do esforço geral de teste necessário para testar produtos da SPLE. O esforço de teste pode ser reduzido maximizando o reuso de teste usando modelos que representam variabilidades entre os produtos. O objetivo da tese é automatizar a geração de compactos conjuntos de testes com alta capacidade de detecção de falhas e baixa redundância de teste entre produtos. Para alcançar tal objetivo, testes equivalentes são identificados para um conjunto de produtos usando conjuntos de teste completos e configuráveis. Duas direções de pesquisa são exploradas, uma centrada no produto e a outra centrada na linha de produto. Foram gerados conjuntos de teste que tenham cobertura de falhas completa a partir de máquinas de estado com e sem restrições de características. A implementação de uma ferramenta foi desenvolvida para automatizar a geração de teste. Além disso, a abordagem proposta foi avaliada usando exemplos, estudos experimentais e um estudo de caso industrial. Os resultados indicam uma redução de esforço de teste de 36% na primeira direção de pesquisa para uma linha com 24 produtos, e na segunda linha de pesquisa uma redução incremental com mais produtos a serem testados. Para 6 produtos uma redução de 15% (do estudo de caso), e para 20 produtos randomicos uma redução de 50% (dos estudos experimentais).
57

A Model-Based AI-Driven Test Generation System

Santiago, Dionny 09 November 2018 (has links)
Achieving high software quality today involves manual analysis, test planning, documentation of testing strategy and test cases, and development of automated test scripts to support regression testing. This thesis is motivated by the opportunity to bridge the gap between current test automation and true test automation by investigating learning-based solutions to software testing. We present an approach that combines a trainable web component classifier, a test case description language, and a trainable test generation and execution system that can learn to generate new test cases. Training data was collected and hand-labeled across 7 systems, 95 web pages, and 17,360 elements. A total of 250 test flows were also manually hand-crafted for training purposes. Various machine learning algorithms were evaluated. Results showed that Random Forest classifiers performed well on several web component classification problems. In addition, Long Short-Term Memory neural networks were able to model and generate new valid test flows.
58

Zpětnovazební funkční verifikace hardware / Feedback Hardware Functional Verification

Santa, Marek January 2011 (has links)
In the development process of digital circuits, it is often not possible to avoid introducing errors into systems that are being developed. Early detection of such errors saves money and time. This project deals with automation of feedback in functional verification of various data processing components. The goal of automatic feedback is not only to shorten the time needed to verify the functionality of a system, but mainly to improve verification coverage of corner cases and thus increase the confidence in the verified system. General functional and formal verification principles and practices are discussed, coverage metrics are presented, limitations of both techniques are mentioned and room for improvement of current status is identified. Design of feedback verification environment using a genetic algorithm is described in detial. The verification results are summarized and evaluated.
59

Program Analyses for Understanding the Behavior and Performance of Traditional and Mobile Object-Oriented Software

Yan, Dacong 20 October 2014 (has links)
No description available.
60

Algorithms and Data Structures for Parametric Analysis of Real-Time Systems / Algorithmen und Datenstrukturen für parametrisierten Analyse von Echt-Zeit Systems

Chamuczynski, Patryk 16 February 2009 (has links)
No description available.

Page generated in 0.1408 seconds