This thesis examines applying formal methods to software testing. Software testing is a critical phase of the software life-cycle which can be very effective if performed rigorously. Formal specifications offer the bases for rigorous testing practices. Not surprisingly, the most immediate use of formal specifications in software testing is as sources of black-box test suites. However, formal specifications have more uses in software testing than merely being sources for test data. We examine these uses, and show how to get more assistance and benefit from formal methods in software testing. At the core of this work is a exible framework in which to conduct specification-based testing. The framework is founded on formal definitions of tests and test suites, which directly addresses important issues in managing software testing. This provides a uniform platform for other applications of formal methods to testing such as analysis and reification of tests, and also for applications beyond testing such as maintenance and specification validation. The framework has to be exible so that any testing strategies can be used. We examine the need to adapt certain strategies to work with the framework and formal specification. Our experiments showed some deficiencies that arise when using derivation strategies on abstract specifications. These deficiencies led us to develop two new specification-based testing strategies based on extensions to existing strate- gies. We demonstrate the framework, strategies, and other applications of formal methods to software testing using three case studies. In each of these, the framework was easy to use. It provided an elegant and powerful means for defining and structuring tests, and a suitable staging ground for other applications of formal methods to software testing. This thesis demonstrates how formal specification techniques can systematise the application of testing strategies, and also how the concepts of software testing can be combined with formal specifications to extend the role of the formal specification in software development.

Made available in DSpace on 2014-06-12T15:52:05Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2008 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Linhas de Produto de Software (LPS) englobam famílias de sistemas desenvolvidos a partir de artefatos reusáveis. Um fator importante durante a manutenção de LPS con- siste em decidir sobre qual mecanismo deve ser utilizado para reestruturar suas variações objetivando melhorar a modularidade de seus artefatos. Devido µa grande variedade de mecanismos, selecionar os corretos pode ser uma tarefa difícil. Por outro lado, selecionar os incorretos pode produzir efeitos negativos no custo de desenvolver a LPS. E importante salientar que este problema existe não somente no nível de código fonte, mas também em outros artefatos como requisitos de software e testes. Assim sendo, para reduzir tal problema no nível de testes automatizados, este trabalho prop~oe um modelo de decisão que ajuda desenvolvedores a escolher mecanismos para reestruturar variações de testes em LPS. Para construir o modelo, algumas variacões encontradas em casos de teste automatizados reais desenvolvidos pela Motorola foram analisadas. Neste caso, os testes servem para testar os sistemas de software dos telefones celulares da Motorola. Os testes lidam com as variacões dos diferentes celulares usando condicionais if-else. Portanto, dada uma variacão baseada em condicionais if-else, o modelo sugere um mecanismo para prover uma melhor modularidade da variacão. Adicionalmente, uma ferramenta para dar suporte aos desenvolvedores de LPS foi desenvolvida. A ferramenta recomenda os mecanismos de acordo com o modelo de decisão proposto. Aplicando o modelo de decisão e os mecanismos sugeridos por ele pode melhorar a modularidade das variações dos casos de teste e remover problemas como códigos dupli- cados. Ademais, mostra-se que a tarefa de reestruturar variações torna-se mais rápida e precisa quando a ferramenta é utilizada

Made available in DSpace on 2014-06-12T15:53:11Z (GMT). No. of bitstreams: 2 arquivo1906_1.pdf: 1728491 bytes, checksum: 711dbaf0713ac324ffe904a6dace38d7 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Albertins de Lima, Lucas; Cezar Alves Sampaio, Augusto. Test case prioritization based on data reuse for Black-box environments. 2009. Dissertação (Mestrado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2009.

LBTest is a learning based-testing tool for black box testing, developed by the software reliability group at KTH. Learning based-testing combines model checking with a learning algorithm that incrementally learns a model of the system under test, which allows for a high degree of automation. This thesis examines the possibilities to use LBTest for testing of electronic control units (ECUs) at Scania. Through two case studies the possibility to formalise ECU requirements and to model ECU applicationsfor LBTest are evaluated. The case studies are followed up with benchmarking against test cases currently in use at Scania. The results of the case studies show that most of the functional requirements can, after reformulation, be formalised for LBTest and that LBTest can find previously undetected defects in ECU software. The benchmarking also shows a high error detection rate for LBTest. Finally, the thesis presents guidelines for requirement formulation and improvements of LBTest are suggested. / LBTest är ett inlärningsbaserat verktyg för black box-testing som har utvecklats av programvarutillförlitghetsgruppen på KTH. Inlärningsbaserad testning kombinerar model checking med en inlärningsalgoritm som stegvis bygger upp en lärd modell av systemet under test, vilket möjliggör en hög grad av automatisering. Denna uppsats undersöker möjligheten att använda LBTest för att testa elektroniska kontrollenheter (ECU:er) på Scania. Genom två fallstudier utvärderas möjligheten att formalisera krav på ECU:er och modellera ECU-applikationer för LBTest. Fallstudierna följs upp med en benchmarking gentemot befintliga testfall på Scania. Resultaten av fallstudierna visar att majoriteten av de funktionella kraven kan formaliseras för LBTest efter en omformulering och att LBTest kan hitta tidigare oupptäckta fel i mjukvaran. Benchmarkingen visar en hög grad av feldetektion för LBTest. I uppsatsen föreslås också riktlinjer för kravformulering och möjliga förbättringar av LBTest.

O teste de software é considerado uma importante atividade na garantia da qualidade de produtos de software. No entanto, há uma carência de profissionais qualificados nessa área. Isso pode ser ocasionado pela dificuldade de ensinar teste de software por meio de abordagens que utilizem apenas aulas teóricas e ferramentas de teste tradicionais. Além disso, há uma desmotivação decorrente do ambiente de trabalho e das estratégias de alocação e responsabilidade desses profissionais nas equipes de desenvolvimento e teste. Para amenizar esses problemas, têm sido utilizado outras abordagens de apoio ao ensino de teste de software, tais como: jogos educacionais, ensino de teste com programação, módulos educacionais, entre outras. O objetivo deste projeto de mestrado foi desenvolver um jogo educacional, denominado Testing Game, para auxiliar o ensino de teste de software, especificamente: teste funcional, teste estrutural e teste de mutação. Para auxiliar o desenvolvimento do Testing Game, foi realizado um mapeamento sistemático para selecionar um motor de jogos. Na primeira versão do jogo foi utilizado o motor de jogos Cocos2D e na segunda versão foi utilizado o Construct 2. Para avaliar a eficiência do Testing Game, realizou-se um estudo de viabilidade com o intuito de avaliar a qualidade com relação à motivação, experiência do usuário e aprendizagem sob o ponto de vista dos estudantes. Além disso, avaliou-se a usabilidade do Testing Game. Aproximadamente 85,64% das pessoas que participaram do estudo avaliaram a qualidade do jogo de forma positiva com relação à motivação, experiência do usuário e aprendizagem sob o ponto de vista dos estudantes. Quanto à usabilidade do jogo, foram identificados poucos problemas, o que possibilita a liberação do jogo. Por meio deste trabalho, percebeu-se que o jogo Testing Game poderia ser utilizado como um recurso complementar de apoio ao ensino de teste de software, e sua efetividade ser avaliada. / Software testing is a relevant activity to provide evidences of qualifty of software products. However, there is a lack of qualified professionals in this area. This can be caused due to difficulty in teaching software testing through approaches that use only theoretical classes traditional tools. In addition, there is a lack of motivation due to the work environment and the strategies of allocation and responsibility of these professionals in development and testing teams. To mitigate these problems, approaches have been used to support software testing education, such as: educational games, integrated teaching of software testing with programming, educational modules, among others. The objective of this masters thesis was to develop an educational game named Testing Game, addressing the following topics: functional testing, structural testing and mutation testing. To support the development of the Testing Game, we performed a systematic mapping aiming at selecting a game engine. In the first game version, we used Cocos2D and in the second one we used Construct 2. To evaluate the efficiency of the game, we conducted a feasibility study to evaluate the quality regarding motivation, user experience and learning from the point of view of the students. Moreover, we also evaluate the usability of the Testing Game. Approximately 85.64% of people who participated in the study assessed the quality of the game in a positive perspective regarding motivation, user experience and learning from the point of view of the students. Regarding the usability of the game, students identified minor problems were identified, which allows the release of the game. Through this work, we realize that the game Testing Game can be used as a complementary resource to support software testing education, and its effectiveness be evaluated.

Throughout its lifetime, software must be changed for many reasons, such as bug fixing, performance tuning, and code restructuring. Testing modified software is the main activity performed to gain confidence that changes behave as they are intended and do not have adverse effects on the rest of the software. A fundamental problem of testing evolving software is determining whether test suites adequately exercise changes and, if not, providing suitable guidance for generating new test inputs that target the modified behavior. Existing techniques evaluate the adequacy of test suites based only on control- and data-flow testing criteria. They do not consider the effects of changes on program states and, thus, are not sufficiently strict to guarantee that the modified behavior is exercised. Also, because of the lack of this guarantee, these techniques can provide only limited guidance for generating new test inputs. This research has developed techniques that will assist testers in testing evolving software and provide confidence in the quality of modified versions. In particular, this research has developed a technique to identify testing requirements that ensure that the test cases satisfying them will result in different program states at preselected parts of the software. This research has also developed supporting techniques for identifying testing requirements. Such techniques include (1) a differencing technique, which computes differences and correspondences between two software versions and (2) two dynamic-impact-analysis techniques, which identify parts of software that are likely affected by changes with respect to a set of executions.

Software testing is an important phase the of software development cycle which reveals faults and ensures correctness of the developed software. Distributed real-time systems are mostly safety critical systems for which the correctness and quality of the software is much more significant. However, majority of the current testing techniques have been developed for sequential (non real-time) software and there is a limited amount of research on testing distributed real-time systems. In this thesis, a proposed approach in the academic literature testing distributed real-time systems using a distributed test architecture is implemented and compared to existing software testing practices in a software development company on a case study. Evaluation of the results show the benefits of using the considered distributed test approach on distributed real-time systems in terms of software correctness.

<p> </p><p>Most software today is concurrent and are used in everything from cell-</p><p>phones, washing machines, cars to aircraft control systems. The reliability</p><p>of the concurrent software may be more or less critical, depending on which</p><p>a.o. domain it is functioning in. Irrespective of domain, the concurrent</p><p>software must be sufficiently reliable.</p><p>It is therefore interesting to study how adaptable test methods for sequential</p><p>software are to test concurrent software. Novel test methods for concurrent</p><p>software can be developed by adapting test methods for sequential software.</p><p>In this dissertation, adaptability factors have been identified by conducting</p><p>a literature survey over state-of-the-art test methods. Directions taken in</p><p>the research of concurrent software testing is described by the survey. The</p><p>survey also demonstrates differences and similarities between test methods.</p><p>Three research contributions has been achieved by this dissertation. First,</p><p>this dissertation presents a survey over state-of-the-art-test methods. The</p><p>second contribution is the identified adaptability factors that should be</p><p>added to a test method for sequential software, that will be adapted to test</p><p>concurrent software. Finally, the third contribution to the field of concurrent</p><p>software testing is the identified future work in areas where test methods for</p><p>concurrent software has not been researched much or at all.</p><p> </p>

abstract / toc / Computer Science and Information Systems / Doctoral / Doctor of Philosophy

Software testing is an expensive process, which is vital in the industry. Construction of the test-data in software testing requires the major cost and knowing which method to use in order to generate the test data is very important. This paper discusses the performance of search-based algorithms (preferably genetic algorithm) versus random testing, in software test-data generation. A factorial experiment is designed so that, we have more than one factor for each experiment we make. Although many researches have been done in the area of automated software testing, this research differs from all of them due to sample programs (SUTs) which are used. Since the program generation is automatic as well, Grammatical Evolution is used to guide the program generations. They are not goal based, but generated according to the grammar we provide, with different levels of complexity. Genetic algorithm is first applied to programs, then we apply random testing. Based on the results which come up, this paper recommends one method to use for software testing, if the SUT has the same conditions as we had in this study. SUTs are not like the sample programs, provided by other studies since they are generated using a grammar.