Model-based testing (MBT) is using a model of expected behavior of the system to automatically generate a set of tests. It aims at reducing the testing cost when compared to the traditional testing techniques. This work focuses on testing a real-world software system using the selected MBT tool OSMO. The tested system is responsible for compiling business rules and it is one of the main components of the Drools platform, developed by Red Hat. The work describes the introduction of MBT considering the good reception from the community of developers, then the creation of compiler input models and evaluation of the newly created test suite. The usage of the MBT resulted in detection of five reported and three potential issues in the tested code. Using the Drools compiler example, the work summarizes the main strengths and also weaknesses of practical use of MBT techniques.

Les systèmes réactifs sont modélisés avec différents types d'automates, tels que les systèmes de transitions symboliques à entrée sortie (IOSTS). L'exécution symbolique d'un IOSTS permet la génération de cas de test qui peuvent être exécutés sur une implantation concrète, afin de déterminer si elle est conforme à son modèle. Dans ce document, nous étendons les IOSTS avec des appels de fonctions utilisateur et analysons leur impact sur le système entier et viceversa. Cette thèse comble l'écart entre une approche basée sur le modèle où les fonctions utilisateur sont abstraites et une approche basée sur le code où les petits morceaux de code sont considérés séparément, indépendamment de la façon dont ils sont combinés. Selon le niveau de connaissance que nous avons sur ces fonctions, elles sont modélisées soit par une spécification complète, soit par une spécification partielle, soit juste comme des boîtes noires fournies sans aucune connaissance. Premièrement, lorsque les fonctions sont partiellement connues, nous utilisons des bouchons définis par des tables contenant des tuples représentatifs des données d'entrée/sortie. L'approche proposée emprunte au test "concolic", l'idée de mélanger l'exécution symbolique avec l'information obtenue à partir d'exécutions concrètes des fonctions (tables). Deuxièmement, si l'utilisateur est prêt à fournir d'autres spécifications, il serait intéressant d'utiliser des représentations plus complètes pour les fonctions. Par conséquent, nous proposons d'abstraire des comportements des fonctions par des contrats pré/post. Ensuite, nous étendons l'exécution symbolique en analysant les fonctions via leurs contrats. Enfin, lorsque les fonctions appelées sont complètement inconnues, nous présentons une approche pour extraire de nouveaux contrats pour eux en explorant les contraintes issues de l'exécution symbolique de l'IOSTS. De tels contrats reflètent les contraintes des fonctions qui rendent possible un certain comportement (exigence). / Reactive systems are modeled with various kinds of automata, such as Input Output Symbolic Transition Systems (IOSTS). Symbolic execution over an IOSTS allows test cases generation that can be executed on a concrete implementation, in order to determine whether it is conforming to its model. In this dissertation, we aim at extending the IOSTS framework with explicit user-defined function calls and analyze their impact on a whole system and vice-versa. The thesis bridges the gap between a model-based approach in which user-defined functions are abstracted away and a code-based approach in which small pieces of code are considered separately regardless of the way they are combined. According to the level of knowledge we have about these functions, they are modeled either by a complete specification, a partial specification, or even just as black-boxes provided without any knowledge. First, when functions are partially known, we use function stubs defined by tables containing representative input/output data tuples. The proposed approach borrows from concolic testing, the idea of mixing symbolic execution with information obtained from instrumented concrete executions (function tables). Second, if the user is willing to provide further specifications, it would be interesting to use more complete representations for called functions. Hence, we propose to abstract function behaviors by means of pre/post contracts. Then we extend symbolic execution by analyzing the functions through their contracts. Finally, when called functions are completely unknown, we present an approach to extract new contracts for them by exploring constraints coming from the IOSTS symbolic execution. Such contracts reflect constraints on the functions that make some behavior (requirement) feasible.

The automatic creation of test cases has been a well-researched area in recent years. Indeed, the industry’s testing procedure still uses the traditional way of manual practices. However, investigations are continued to deliver new methods, but research results have not been fully adopted. In this paper, the investigated method applies the model-based testing (MBT) method to evaluate the ability to automate the creation of hardware-in-the-loop (HIL) test cases, where generated tests are created using MBT tools. The tools’ properties were compared to each other through a literature study, with the result of selecting tools to be used in a case study, and the tools selected were GraphWalker and MoMuT. The generated test cases perform similarly to their manual counterparts regarding how the test cases achieved full requirements coverage. When comparing the effort needed for applying the methods, a comparable effort is required for creating the first iteration, while with every subsequent update, MBT will require less effort compared to the manual process. Both methods achieve 100% requirements coverage, and since manual testing is created and executed by humans, some requirements are favoured over others due to company demands, while MBT tests will be generated randomly.In addition, a comparison between the used tools showcased the differences in the models’ design and their test case generation. The comparison showed that GraphWalker has a more straightforward design method and is better suited for smaller systems, while’s MoMuT can handle more complex systems but has a more involved design method.The results of the thesis showed that using MBT tools proved helpful as it covers the system requirements, can be executed in HIL and helps discover faults within the requirements and HIL system. These facts satisfy the companies’ demands. This thesis shows a promising improvement in automating the test process within the vehicular domain.

Yes / Engineering design in general and system design of embedded software have a direct impact on the final engineering product and the software implementation, respectively. Guaranteeing that the models utilised meet the specified requirements is beneficial in detecting misbehaviour and software flaws. This requires an integrated approach, combining verification and model-based testing methodology and notations and methods from system engineering and software engineering. In this paper, we propose a model-based approach integrating various notations utilised in the functional design of complex systems with formal verification and testing. We illustrate our approach on the cruise control system of an e-Bike case study.

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.

As técnicas de teste podem ser divididas, num primeiro nível, naquelas baseadas no código (caixa branca) e naquelas baseadas na especificação (caixa preta ou funcionais). Nenhuma delas é completa pois visam a identificar tipos diferentes de defeitos e a sua utilização em conjunto pode elevar o nível de confiabilidade das aplicações. Assim, tornam-se importantes estudos que contribuam para um melhor entendimento da relação existente entre técnicas funcionais e estruturais, como elas se complementam e como podem ser utilizadas em conjunto. Este trabalho está inserido no contexto do projeto PLAVIS (Plataforma para Validação e Integração de Software em Aplicações Espaciais), e tem como objetivo realizar um estudo comparativo entre as técnicas de geração de casos de teste funcionais (baseadas nas especificações formais) e os critérios estruturais baseados em fluxo de controle e fluxo de dados, aplicados nas implementações. Num contexto específico, esse estudo deve fornecer dados de como se relacionam essas duas técnicas (funcional e estrutural) gerando subsídios para sua utilização em conjunto. Num contexto mais amplo - o do projeto PLAVIS - visa a estabelecer uma estratégia de teste baseada em critérios funcionais e estruturais e que possam, juntamente com as ferramentas que dão suporte a eles, compor um ambiente de teste disponível à utilização em aplicações espaciais dentro do INPE / Testing techniques can be divided, in high level, in code-based ones (white box) and specification based ones (black box). None of them are complete as they intend to identify different kinds of faults. The use of them together can increase the application confidence level. Thus, it is important to investigate the relationship between structural testing techniques and functional testing techniques, how they complete themselves and how they can be used together. This paper was developed in the context of the Plavis (PLAtform of software Validation & Integration on Space systems) project. This project provides comparative studies between functional generation testing techniques (based on formal specifications) and structural generation testing techniques, such as control-flow and data-flow criteria, applied in the implementation. In a specific context, this study provides data about the relationship between these techniques and how they can be used together. In the context of the Plavis project, the goal is to provide a testing strategy, based on functional and structural criteria, and a set of tools, composing a testing environment to be used in Space Applications projects, at INPE

Abstract Testing is an important part of quality assurance, and the use of agile processes, continuous integration and DevOps is increasing the pressure for automating all aspects of testing. Testing through graphical user interfaces (GUIs) is commonly automated by scripts that are captured or manually created with a script editor, automating the execution of test cases. A major challenge with script-based GUI test automation is the manual effort required for maintaining the scripts when the GUI changes. Model-based testing (MBT) is an approach for automating also the design of test cases. Traditionally, models for MBT are designed manually with a modelling tool, and an MBT tool is used for generating abstract test cases from the model. Then, an adapter is implemented to translate the abstract test cases into concrete test cases that can be executed on system under test (SUT). When the GUI changes, the model has to be updated and the test cases can be generated from the updated model, reducing the maintenance effort. However, designing models and implementing adapters requires effort and specialized expertise. The main research questions of this thesis are 1) how to automatically extract state-based models of software systems with GUI, and 2) how to use the extracted models to automate testing. Our focus is on using dynamic analysis through the GUI during automated exploration of the system, and we concentrate on desktop applications. Our results show that extracting state models through GUI is possible and the models can be used to generate regression test cases, but a more promising approach is to use model comparison on extracted models of consequent system versions to automatically detect changes between the versions. / Tiivistelmä Testaaminen on tärkeä osa laadun varmistusta. Ketterät kehitysprosessit ja jatkuva integrointi lisäävät tarvetta automatisoida kaikki testauksen osa-alueet. Testaus graafisten käyttöliittymien kautta automatisoidaan yleensä skripteinä, jotka luodaan joko tallentamalla manuaalista testausta tai kirjoittamalla käyttäen skriptieditoria. Tällöin scriptit automatisoivat testitapausten suorittamista. Muutokset graafisessa käyttöliittymässä vaativat scriptien päivittämistä ja scriptien ylläpitoon kuluva työmäärä on iso ongelma. Mallipohjaisessa testauksessa automatisoidaan testien suorittamisen lisäksi myös testitapausten suunnittelu. Perinteisesti mallipohjaisessa testauksessa mallit suunnitellaan manuaalisesti käyttämällä mallinnustyökalua, ja mallista luodaan abstrakteja testitapauksia automaattisesti mallipohjaisen testauksen työkalun avulla. Sen jälkeen implementoidaan adapteri, joka muuttaa abstraktit testitapaukset konkreettisiksi, jotta ne voidaan suorittaa testattavassa järjestelmässä. Kun testattava graafinen käyttöliittymä muuttuu, vain mallia täytyy päivittää ja testitapaukset voidaan luoda automaattisesti uudelleen, vähentäen ylläpitoon käytettävää työmäärää. Mallien suunnittelu ja adapterien implementointi vaatii kuitenkin huomattavan työmäärän ja erikoisosaamista. Tämä väitöskirja tutkii 1) voidaanko tilamalleja luoda automaattisesti järjestelmistä, joissa on graafinen käyttöliittymä, ja 2) voidaanko automaattisesti luotuja tilamalleja käyttää testauksen automatisointiin. Tutkimus keskittyy työpöytäsovelluksiin ja dynaamisen analyysin käyttämiseen graafisen käyttöliittymän kautta järjestelmän automatisoidun läpikäynnin aikana. Tutkimustulokset osoittavat, että tilamallien automaattinen luominen graafisen käyttöliittymän kautta on mahdollista, ja malleja voidaan käyttää testitapausten generointiin regressiotestauksessa. Lupaavampi lähestymistapa on kuitenkin vertailla malleja, jotka on luotu järjestelmän peräkkäisistä versioista, ja havaita versioiden väliset muutokset automaattisesti.

With modern computer systems becoming more and more complicated, theimportance of rigorous testing to ensure the quality of the product increases.This, however, means that the cost to perform tests also increases. In orderto address this problem, a lot of research has been conducted during thelast years to find a more automated way of testing software systems. Inthis thesis, different algorithms to automatically explore and test a systemhave been implemented and evaluated. In addition to this, a second setof algorithms have been implemented with the objective to isolate whichinteractions with the system were responsible for a failure. These algorithmswere also evaluated and compared against each other. In the first evaluationtwo explorers, which I called DeBruijn and LStarExplorer, were consideredsuperior to the other. The first used a DeBruijn sequence to brute forcea solution while the second used the L*-algorithm to build an FSM overthe system under test. This FSM could then be used to provide a moreaccurate description for when the failure occurred. The result from thesecond evaluation were two reducers which both tried to recreate a failureby first applying interactions performed just before the failure occurred. Ifthis was not successful, they tried interactions further and further away, untilthe failure was triggered. In addition to this, the thesis contains descriptionsabout the framework used to run the different strategies. / D ̊a v ̊ara moderna datasystem blir allt mer komplicerade,  ̈okar detta st ̈andigtbehovet av rigor ̈osa tester f ̈or att s ̈akerst ̈alla kvaliteten p ̊a den slutgiltiga pro-dukten. Det h ̈ar inneb ̈ar dock att kostnaden f ̈or att utf ̈ora testerna ocks ̊ao  ̈ kar. F ̈or att f ̈ors ̈oka hitta en l ̈osning p ̊a det h ̈ar problemet har forsknin-gen under senare tid arbetat med att ta fram automatiserade metoder atttesta mjukvarusystem. I den h ̈ar uppsatsen har olika algoritmer, f ̈or attutforska och testa ett system, implementerats och utv ̈arderats. D ̈arut ̈overhar ocks ̊a en grupp algoritmer implementerats som ska kunna isolera vilkainteraktioner med ett system som f ̊ar det att fallera.  ̈aven dessa algoritmerhar utv ̈arderats och testats mot varandra. Resultatet fr ̊an det f ̈orsta ex-perimentet var tv ̊a explorers, h ̈ar kallade DeBruijn och LStarExplorer, somvisade sig vara b ̈attre  ̈an de andra. Den f ̈orsta av dessa anv ̈ande en DeBruijn-sekvens f ̈or att hitta felen, medan den andra anv ̈ande en L*-algoritm f ̈or attbygga upp en FSM  ̈over systemet. Den h ̈ar FSM:en kunde sedan anv ̈andasf ̈or att mer precist beskriva n ̈ar felet uppstod. Resultatet fr ̊an det andraexperimentet var tv ̊a reducers, vilka b ̊ada f ̈ors ̈okte  ̊aterskapa fel genom attf ̈orst applicera interaktioner som ursprungligen utf ̈ordes percis innan feletuppstod. Om felet inte kunde  ̊aterskapas p ̊a detta s ̈att, fortsatte de medatt applicera interaktioner l ̈angre bort tills felet kunde  ̊aterskapas. Ut ̈overdetta inneh ̊aller uppsatsen ocks ̊a beskrivningar av ramverken som anv ̈andsf ̈or att k ̈ora de olika strategierna.

Modeliais paremtas testavimas tampa vis populiaresnis. Sudėtingos programinės įrangos kokybės užtikrinimas ir modeliais orientuotas sistemų kūrimas yra pagrindinės šio testavimo būdo išpopuliarėjimo priežastys. Pagrindiniai šio darbo tikslai yra modeliais paremtų testavimo įrankių analizė ir jų tobulinimo galimybės. Darbe naudojama daugiau nei dešimt įvairių įrankių vertinimo kriterijų. Analizuojama testų padengimo kriterijų pritaikymo ir tobulinimo galimybės. Analizuojamos modeliais paremto proceso problemos ir pateikiami sprendimo būdai. Atlikta detali testų kūrimo kriterijų ir modelio perėjimo algoritmų analizė. Atlikus detalę kriterijų ir modelio perėjimo algoritmų analizę, pateikiama kriterijų apjungimo privalumai ir kaip naudojant įvairius kriterijus galima valdyti testų kūrimo procesą ir siekti 100 procentinio modelio padengimo. Pateikiama ir detaliai išanalizuojama kriterijų kūrimo metodika, kurią galim taikyti testavimo įrankiuose. / Model-based testing has become increasingly popular in recent years. Major reasons include the need for quality assurance for increasingly complex systems and the emerging model-centric development paradigm. The present thesis aims at analysing model-based testing tools and presents the possibilities for their improvement. More than dozen criteria are applied in analysing selected tools. The paper analyses the application of testing coverage criteria and presents their possible improvements. The problems occurring in the model-based testing process are being analysed and the solutions presented. The study contains an in-depth analysis of test coverage criteria and model traversal algorithms. A thorough analysis of test criteria and model traversal algorithms being performed, the advantages of the integration of test criteria are presented. Furthermore, a solution for managing the development process of test cases as well as pursuing a hundred percent model coverage is proposed. The paper presents a comprehensive analysis of test criteria development methodology that could be applied in testing tools.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-27T18:21:34Z No. of bitstreams: 1 LAÍSA HELENA OLIVEIRA DO NASCIMENTO - DISS PPGCC 2008..pdf: 1446971 bytes, checksum: 3622ab4c366ab0a686c4f32d688c13b6 (MD5) / Made available in DSpace on 2018-08-27T18:21:34Z (GMT). No. of bitstreams: 1 LAÍSA HELENA OLIVEIRA DO NASCIMENTO - DISS PPGCC 2008..pdf: 1446971 bytes, checksum: 3622ab4c366ab0a686c4f32d688c13b6 (MD5) Previous issue date: 2008-02-28 / Processos de teste de software vêm ganhando cada vez mais espaço na indústria. Empresas têm investindo na definição e formalização dos seus processos e em meio a essa mudança de comportamento, Model-Based Testing (MBT) apresenta-se como uma técnica promissora de teste. No entanto, a utilização de MBT ainda é baixa e pesquisadores têm focado em maneiras de superar as barreiras para que se obtenha uma adoção maior por parte da indústria. O mundo empresarial é movido a processos e resultados. Dessa forma, o uso de MBT precisa se adaptar aos processos existentes, e estudos de caso que evidenciem as vantagens de sua utilização precisam ser conduzidos. Neste trabalho, o paradigma Goal Question Metric é utilizado na definição de modelos de medição que têm como foco principal a avaliação e o acompanhamento do desempenho de MBT sem causar impacto ao processo de teste já existente. Os modelos de medição consideram métricas como esforço, percentual de requisitos testáveis cobertos, percentual de casos de teste modificados, percentual de falhas,dentre outros. Os modelos não estão atrelados ao processo de MBT apresentado, podendo ser aplicados em qualquer processo que permita a coleta dos dados necessários para o cálculo das métricas. Para validar os modelos, estudos de caso foram conduzidos dentro do ambiente de testes da Motorola. / Software testing processes have become more common in industry. Companies are investing on the definition and the formalization of their test processes and, in this context, Model-Based Testing (MBT) appears as an interesting testing technique. However, industrial adoption of MBT remains low and researchers are also focusing on how to beat the barriers to wide adoption. Processes and results move the business world so, MBT processes must be adaptable to actual testing processes. For this, experiments to evaluate the results achieved with its use must be conduct. In this work, measurement models based on the Goal Question Metric methodology are proposed. The purpose is evaluating the use of MBT without increasing actual testing process costs. The models focus on aspects as effort, testable requirements coverage, modified test cases, failures, among others. The models are not associated with the MBT process presented. They can be applied with any process that allows metrics collection. In order to validate the measurement models, case studies were conducted into Motorola testing environment.