Made available in DSpace on 2014-06-12T15:57:28Z (GMT). No. of bitstreams: 2 arquivo3199_1.pdf: 729356 bytes, checksum: 6c269a282f3e408a30566d12c64fac0e (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Os contratos (modelos que descrevem mais detalhadamente a arquitetura e os componentes) podem ser utilizados para a construção de softwares corretos. Esta construção pode ser realizada através do (1) cálculo de refinamento, (2) refinamento da estratégia e (3) fazendo a geração automática de código. Embora (1) e (2) são soluções corretamente comprovadas, eles requerem bastante esforço. Por outro lado, (3) é uma solução mais simples para derivação do código. No entanto, esta solução não pode fornecer um código confiável em relação aos seus contratos (ao menos que se comprove que o gerador de código é correto). Este trabalho propõe uma estratégia de testes baseados em modelos para verificar se determinado gerador de código é correto. A estratégia inicia-se com JML (linguagem baseada em contrato utilizada no Java) usando como estudo de caso o JavaCard, JMLe (um gerador de código baseado em JML) e o Jartege (gerador de testes baseados em modelos). Além disso, através deste trabalho é realizado um experimento onde é investigado o número de erros encontrados no jmle variando os valores do parâmetros do Jartege no nosso estudo de caso

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-10-11T20:48:07Z No. of bitstreams: 1 ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-10-14T00:17:49Z (GMT) No. of bitstreams: 1 ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Made available in DSpace on 2016-10-14T00:17:49Z (GMT). No. of bitstreams: 1 ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) Previous issue date: 2016-04-14 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / Sistemas de software esta?o presentes em grande parte das nossas vidas atualmente e, mais do que nunca, eles requerem um alto ni?vel de confiabilidade. Existem va?rias te?cnicas de Ver- ificac?a?o e Validac?a?o (V&V) de software que se preocupam com controle de qualidade, segu- ranc?a, robustez e confiabilidade; as mais conhecidas sa?o Testes de Software e Me?todos For- mais. Me?todos formais e testes sa?o te?cnicas que podem se complementar. Enquanto me?to- dos formais prove?em mecanismos confia?veis para raciocinar sobre o sistema em um ni?vel mais abstrato, te?cnicas de teste ainda sa?o necessa?rias para uma validac?a?o mais profunda e sa?o frenquentemente requeridas por orga?os de certificac?a?o. Levando isto em considerac?a?o, BETA prove? uma abordagem de testes baseada em modelos para o Me?todo B, suportada por uma ferramenta, que e? capaz de gerar testes de unidade a partir de ma?quinas abstratas B. Nesta tese de doutorado apresentamos melhorias realizadas em BETA e novos estudos de caso realizados para avalia?-la. Dentre as melhorias, integramos crite?rios de cobertura lo?gicos a? abordagem, revisamos os crite?rios de cobertura baseados em espac?o de entrada que ja? eram suportados e aperfeic?oamos as u?ltimas etapas do processo de gerac?a?o de testes. A abordagem agora suporta a gerac?a?o automa?tica de dados para os ora?culos e prea?mbulos para os casos de teste; ela tambe?m possui uma funcionalidade para concretizac?a?o dos da- dos de teste e um mo?dulo para gerar scripts de teste executa?veis automaticamente. Outro objetivo desta tese foi realizar estudos de caso mais complexos utilizando BETA e avaliar a qualidade dos casos de teste que a abordagem produz. Estes estudos de caso foram os primeiros a avaliar o processo de gerac?a?o de testes por completo, desde a especificac?a?o dos casos de teste ate? a sua implementac?a?o e execuc?a?o. Em nossos u?ltimos experimentos, analisamos a qualidade dos casos de teste gerados por BETA, considerando cada crite?rio de cobertura suportado, utilizando me?tricas de cobertuda de co?digo como cobertura de in- struc?o?es e ramificac?o?es. Tambe?m utilizamos testes de mutac?a?o para avaliar a capacidade dos casos de teste de detectar faltas na implementac?a?o dos modelos. O resultados obtidos foram promissores mostrando que BETA e? capaz de detectar faltas introduzidas por progra- madores ou geradores de co?digo e que a abordagem pode obter bons resultados de cobertura para a implementac?a?o de um sistema baseado em modelos B. / Software systems are a big part of our lives and, more than ever, they require a high level of reliability. There are many software Verification and Validation (V&V) techniques that are concerned with quality control, security, robustness, and reliability; the most widely known are Software Testing and Formal Methods. Formal methods and testing are techniques that can complement each other. While formal methods provide sound mechanisms to reason about the system at a more abstract level, testing techniques are still necessary for a more in-depth validation of the system and are often required by certification standards. Taking this into consideration, BETA provides a tool-supported, model-based testing approach for the B Method that is capable of generating unit tests from abstract B machines. In this thesis, we present improvements made in the BETA approach and tool, and new cases studies used to evaluate them. Among these improvements, we integrated logical coverage criteria into the approach, reviewed the input space criteria that was already supported, and enhanced the final steps of the test generation process. The approach now has support for automatic generation of oracle data and test case preambles, it has a feature for test data concretization, and a module that automatically generates executable test scripts. Another objective of this thesis was to perform more complex case studies using BETA and assess the quality of the test cases it produces. These case studies were the first to evaluate the test generation process as a whole, from test case design to implementation and execution. In our last experiments, we assessed the quality of the test cases generated by BETA, considering each coverage criteria it supports, using code coverage metrics such as statement and branch coverage. We also used mutation testing to evaluate the ability of the generated test cases to identify faults in the model?s implementation. The results obtained were promising, showing that BETA is capable of detecting faults introduced by a programmer or code generation tool and that it can achieve good coverage results for a system?s implementation based on a B model.

Made available in DSpace on 2014-12-17T15:47:51Z (GMT). No. of bitstreams: 1 FernandaMS_DISSERT_cad.pdf: 1351543 bytes, checksum: 27a89b596f5bafb661e158d68cfc729c (MD5) Previous issue date: 2010-03-29 / With the increasing complexity of software systems, there is also an increased concern about its faults. These faults can cause financial losses and even loss of life. Therefore, we propose in this paper the minimization of faults in software by using formally specified tests. The combination of testing and formal specifications is gaining strength in searches mainly through the MBT (Model-Based Testing). The development of software from formal specifications, when the whole process of refinement is done rigorously, ensures that what is specified in the application will be implemented. Thus, the implementation generated from these specifications would accurately depict what was specified. But not always the specification is refined to the level of implementation and code generation, and in these cases the tests generated from the specification tend to find fault. Additionally, the generation of so-called "invalid tests", ie tests that exercise the application scenarios that were not addressed in the specification, complements more significantly the formal development process. Therefore, this paper proposes a method for generating tests from B formal specifications. This method was structured in pseudo-code. The method is based on the systematization of the techniques of black box testing of boundary value analysis, equivalence partitioning, as well as the technique of orthogonal pairs. The method was applied to a B specification and B test machines that generate test cases independent of implementation language were generated. Aiming to validate the method, test cases were transformed manually in JUnit test cases and the application, created from the B specification and developed in Java, was tested. Faults were found with the execution of the JUnit test cases / Com o crescente aumento da complexidade dos sistemas de software, h? tamb?m um aumento na preocupa??o com suas falhas. Essas falhas podem causar preju?zos financeiros e at? preju?zos de vida. Sendo assim, propomos neste trabalho a minimiza??o de falhas atrav?s de testes em softwares especificados formalmente. A conjun??o de testes e especifica??es formais vem ganhando for?a na academia principalmente atrav?s dos TBM (Testes Baseados em Modelos). O desenvolvimento de software a partir de especifica??es formais, quando todo o processo de refinamento ? feito rigorosamente, garante que o que est? especificado ser? implementado na aplica??o. Sendo assim, a implementa??o gerada a partir destas especifica??es iria retratar fielmente o que estaria especificado. Mas nem sempre a especifica??o ? refinada at? o n?vel de implementa??o e gera??o de c?digo, e nesses casos os testes gerados a partir da especifica??o tendem a encontrar falhas. Adicionalmente, a gera??o dos chamados testes inv?lidos , ou seja, testes que exercitem cen?rios da aplica??o que n?o foram tratados na especifica??o, complementa mais significativamente o processo de desenvolvimento formal. Sendo assim, neste trabalho ? proposto um m?todo para gera??o de testes a partir de especifica??es formais B. Este m?todo foi estruturado em pseudo-c?digo. O m?todo se baseia na sistematiza??o das t?cnicas de testes caixa preta da an?lise do valor limite, particionamento de equival?ncia, bem como da t?cnica dos pares ortogonais. O m?todo foi aplicado em uma especifica??o B e foram geradas m?quinas B de teste que geram casos de teste independentes de linguagem de implementa??o. Com o intuito de valida??o do m?todo, os casos de teste foram transformados manualmente em casos de teste do JUnit e a aplica??o, criada a partir da especifica??o B, e desenvolvida em Java foi testada. Foram encontradas falhas com a execu??o dos casos de teste JUnit

Made available in DSpace on 2014-12-17T15:48:00Z (GMT). No. of bitstreams: 1 ErnestoCBM_DISSERT.pdf: 1152535 bytes, checksum: a61c509f155d27fa9ab04bc69c4607e8 (MD5) Previous issue date: 2012-02-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies / M?todos formais e testes s?o ferramentas para obten??o e controle de qualidade de software. Quando utilizadas em conjunto, elas prov?em mecanismos para especifica??o, verifica??o e detec??o de falhas de um software. Apesar de permitir que sistemas sejam matematicamente verificados, m?todos formais n?o s?o suficientes pra garantir que um sistema esteja livre de defeitos, logo, t?cnicas de teste de software s?o necess?rias para completar o processo de verifica??o e valida??o de um sistema. T?cnicas de Testes Baseados em Modelos permitem que testes sejam gerados a partir de outros artefatos de software como especifica??es e modelos abstratos. Ao utilizarmos especifica??es formais como base para a cria??o de testes, podemos gerar testes de melhor qualidade pois estas especifica??es costumam ser precisas e livres de ambiguidade. Fernanda Souza (2009) prop?s um m?todo para definir casos de teste a partir de especifica??es do M?todo B. Este m?todo utilizava informa??es do invariante de uma m?quina e das pr?-condi??es de uma opera??o para definir casos de teste positivos e negativos para tal opera??o, atrav?s de t?cnicas baseadas em particionamento em classes de equival?ncia e an?lise de valor limite. No entanto, a proposta de 2009 n?o inclu?a automa??o e possu?a algumas defici?ncias conceituais como, por exemplo, n?o se encaixar exatamente em uma classifica??o de crit?rios de cobertura bem definida. Iniciamos nosso trabalho com um estudo de caso que aplicou o m?todo a um exemplo de especifica??o B proveniente da ind?stria. A partir deste estudo obtivemos subs?dios para o aperfei?o?-lo. Em nosso trabalho aperfei?oamos o m?todo proposto, reescrevendo e adicionando caracter?sticas para torn?-lo compat?vel com uma classifica??o de testes utilizada pela comunidade. O m?todo tamb?m foi melhorado para suportar especifica??es estruturadas em v?rios componentes, utilizar informa??es sobre o comportamento da opera??o durante a cria??o de casos de teste e utilizar novos crit?rios de cobertura. Al?m disso, implementamos uma ferramenta para automatiz?-lo e o submetemos a estudos de caso mais complexos

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.