Access Control (AC) is a major pillar in software security. In short, AC ensures that only intended users can access resources and only the required access to accomplish some task will be given. In this context, Role Based Access Control (RBAC) has been established as one of the most important paradigms of access control. In an organization, users receive responsibilities and privileges through roles and, in AC systems implementing RBAC, permissions are granted through roles assigned to users. Despite the apparent simplicity, mistakes can occur during the development of RBAC systems and lead to faults or either security breaches. Therefore, a careful verification and validation process becomes necessary. Access control testing aims at showing divergences between the actual and the intended behavior of access control mechanisms. Model Based Testing (MBT) is a variant of testing that relies on explicit models, such as Finite State Machines (FSM), for automatizing test generation. MBT has been successfully used for testing functional requirements; however, there is still lacking investigations on testing non-functional requirements, such as access control, specially in test criteria. In this Master Dissertation, two aspects of MBT of RBAC were investigated: FSM-based testing methods on RBAC; and Test prioritization in the domain of RBAC. At first, one recent (SPY) and two traditional (W and HSI) FSM-based testing methods were compared on RBAC policies specified as FSM models. The characteristics (number of resets, average test case length and test suite length) and the effectiveness of test suites generated from the W, HSI and SPY methods to five different RBAC policies were analyzed at an experiment. Later, three test prioritization methods were compared using the test suites generated in the previous investigation. A prioritization criteria based on RBAC similarity was introduced and compared to random prioritization and simple similarity. The obtained results pointed out that the SPY method outperformed W and HSI methods on RBAC domain. The RBAC similarity also achieved an Average Percentage Faults Detected (APFD) higher than the other approaches. / Controle de Acesso (CA) é um dos principais pilares da segurança da informação. Em resumo, CA permite assegurar que somente usuários habilitados terão acesso aos recursos de um sistema, e somente o acesso necessário para a realização de uma dada tarefa será disponibilizado. Neste contexto, o controle de acesso baseado em papel (do inglês, Role Based Access Control - RBAC) tem se estabelecido como um dos mais importante paradigmas de controle de acesso. Em uma organização, usuários recebem responsabilidades por meio de cargos e papéis que eles exercem e, em sistemas RBAC, permissões são distribuídas por meio de papéis atribuídos aos usuários. Apesar da aparente simplicidade, enganos podem ocorrer no desenvolvimento de sistemas RBAC e gerar falhas ou até mesmo brechas de segurança. Dessa forma, processos de verificação e validação tornam-se necessários. Teste de CA visa identificar divergências entre a especificação e o comportamento apresentado por um mecanismo de CA. Teste Baseado em Modelos (TBM) é uma variante de teste de software que se baseia em modelos explícitos de especificação para automatizar a geração de casos testes. TBM tem sido aplicado com sucesso no teste funcional, entretanto, ainda existem lacunas de pesquisa no TBM de requisitos não funcionais, tais como controle de acesso, especialmente de critérios de teste. Nesta dissertação de mestrado, dois aspectos do TBM de RBAC são investigados: métodos de geração de teste baseados em Máquinas de Estados Finitos (MEF) para RBAC; e priorização de testes para RBAC. Inicialmente, dois métodos tradicionais de geração de teste, W e HSI, foram comparados ao método de teste mais recente, SPY, em um experimento usando políticas RBAC especificadas como MEFs. As características (número de resets, comprimento médio dos casos de teste e comprimento do conjunto de teste) e a efetividade dos conjuntos de teste gerados por cada método para cinco políticas RBAC foram analisadas. Posteriormente, três métodos de priorização de testes foram comparados usando os conjuntos de teste gerados no experimento anterior. Neste caso, um critério baseado em similaridade RBAC foi proposto e comparado com a priorização aleatória e baseada em similaridade simples. Os resultados obtidos mostraram que o método SPY conseguiu superar os métodos W e HSI no teste de sistemas RBAC. A similaridade RBAC também alcançou uma detecção de defeitos superior.

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).

Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely re exive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as an MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., \"every time the agent does X, it will do Y later\"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS\'s and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or an inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose with respect to the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again. In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into an MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach. / Sistemas multi-agentes (SMAs) podem ser usados para modelar fenômenos que podem ser decompostos em diversos agentes que interagem entre si dentro de um ambiente. Em particular, eles podem ser usados para modelar sociedades humanas e animais, com a finalidade de se analisar as suas propriedades computacionalmente. Esta tese trata da análise automatizada de um tipo particular de tais modelos sociais, a saber, aqueles baseados em princípios behavioristas, o que contrasta com as abordagens cognitivas mais dominante na literatura de SMAs. A principal característica das teorias behaviorista é a ênfase na descrição do comportamento em termos da interação entre agentes e seu ambiente. Desta forma, não apenas ações refl exivas, mas também de aprendizado, motivações, e as emoções podem ser definidas. Mais especificamente, nesta tese apresentamos uma arquitetura de agentes formal (especificada através da Notação Z) baseada na teoria da Análise do Comportamento de B. F. Skinner, e fornecemos uma noção adequada e formal de ambiente (com base na álgebra de processos pi-calculus) para colocar tais agentes juntos em um SMA. Simulações são freqüentemente utilizadas para se analisar SMAs. As técnicas envolvidas tipicamente consistem em simular um SMA diversas vezes, seja para coletar estatísticas, seja para observar o que acontece através de animações. Contudo, simulações podem ser usadas de forma a pertmitir a realização de verificações automatizadas do SMA caso sejam entendidas como explorações de grandes espaços-de-estados. Nesta tese propomos uma técnica de verificação baseada nessa observação, que consiste em simular um SMA de uma forma guiada, a fim de se determinar se uma dada hipótese sobre ele é verdadeira ou não. Para tal fim, tiramos proveito da importância que os ambientes têm nesta tese: a especificação formal do ambiente de um SMA serve para calcular as evoluções possíveis do SMA como um sistema de transição, estabelecendo assim o espaço-de-estados a ser investigado. Neste cálculo, os agentes são levados em conta simulando-os, a fim de determinar, em cada estado do ambiente, quais são suas ações. Cada execução da simulação é uma seqüência de estados nesse espaço-de-estados, que é calculado em tempo de execução, conforme a simulação progride. A hipótese a ser investigada, por sua vez, é dada como um outro sistema de transição, chamado propósito de simulação, o qual define as simulações desejáveis e indesejáveis (e.g., \"sempre que o agente fizer X, ele fará Y depois\"). Em seguida, é possível verificar se o SMA satisfaz o propósito de simulação de acordo com uma série de relações de satisfatibilidade precisamente definidas. Algoritmicamente, isso corresponde a construir um produto síncrono desses dois sistemas de transições (i.e., o do SMA e o do propósito de simulação) em tempo de execução e usá-lo para operar um simulador. Ou seja, o propósito de simulação é usado para guiar o simulador, de modo que somente os estados relevantes sejam efetivamente simulados. Ao terminar, um tal algoritmo pode fornecer um veredito conclusivo ou inconclusivo. Se conclusivo, descobre-se se o SMA satisfaz ou não o propósito de simulação com relação às observações feitas durante as simulações. Se inconclusivo, é possível realizar alguns ajustes e tentar novamente. em resumo, portanto, nesta tese propomos quatro novos elementos: (i) uma arquitetura de agente, (ii) uma especificação formal do ambiente desses agentes, de modo que possam ser compostos em um SMA, (iii) uma estrutura para descrever a propriedade de interesse, a qual chamamos de propósito de simulação, e (iv) uma técnica para se analisar formalmente o SMA resultante com relação a um propósito de simulação. Esses elementos estão implementados em uma ferramenta, denominada Simulador Formalmente Guiado (FGS, do inglês Formally Guided Simulator). Estudos de caso executáveis no FGS são fornecidos para ilustrar a abordagem.

O teste de software engloba diferentes técnicas, métodos e conceitos capazes de garantir a qualidade dos mais variados tipos de sistemas. Dentre tais técnicas, encontra-se o teste baseado em Máquinas de Estados Finitos (MEFs), que visa a garantir a conformidade entre a implementação e a especificação de um software. Com esse propósito, diversos métodos foram propostos para a geração de seqüências de verificação que garantam cobertura total das possíveis falhas existentes em uma implementação. A maioria dos métodos conhecidos são baseados na utilização de seqüências de distinção. Esse recurso, porem, não existe para toda MEF. Alguns métodos buscam a geração de seqüências de verificação baseados em recursos alternativos as seqüências de distinção, contudo, as seqüências geradas são exponencialmente longas. Este trabalho apresenta um método para geração de seqüências de verificação que visa a reduzir o tamanho das seqüências geradas para o domínio de MEFs que não dispõem de seqüência de distinção. Para isso, o método proposto baseia-se na utilização de conjuntos de distinção. Uma avaliação experimental foi realizada afim de mensurar a redução proporcionada pelo método proposto em relação aos principais métodos existentes na literatura. Com esse intuito, foram geradas MEFs aleatórias sob a perspectiva diferentes fatores. Em relação a variação do número de estados, os resultados indicaram reduções acima de 99; 5% em comparação com os métodos existentes, quando analisadas 75% das MEFs geradas / Software testing involves several techniques, methods, and concepts employed to guarantee a high level of quality in different application domains. Among such techniques, Finite State Machine (FSM) based testing aims to guarantee the conformance between the implementation and the specification of a system under test. In this context, several methods were proposed to generate checking sequences that cover all the possible faults existing in an implementation. Most of these methods are based on a special sequence, named distinguishing sequence, which does not exist for every minimal machine. Some methods were proposed to generate checking sequences based on alternative solutions in order to be applied on FSMs that do not have distinguishing sequences. However, these methods generate checking sequences exponentially long. This work proposes a method to generate checking sequences using identification sets. These sets exist for every minimal FSM and also lead to shorter checking sequences. We conducted an experimental study to compare the proposed method with the main existing methods. In the experiments, we used random FSMs that have different configurations of states, inputs, and outputs. Concerning the variation of number of states, the results show reductions higher than 99:5% in comparison with the existing methods for 75% of the experimented machines

A realização de atividades de teste é indispensável para a garantia da qualidade de um produto e para a identificação de defeitos, diminuindo custos de manutenção e evitando ao máximo o risco do cliente encontrar esses defeitos. Nessa linha, testes baseados em modelos têm se mostrado atrativos, pois o custo de geração de casos de testes e de correção de defeitos tende a ser menor. Devido à sua simplicidade conceitual e expressividade na descrição do comportamento de um sistema, um dos modelos mais usados e pesquisados na área de teste baseado em modelos são as Máquinas de Estados Finitos (MEFs). Por meio de MEFs e com apoio de ferramentas apropriadas, a geração de casos de testes para avaliar os comportamentos esperados de um sistema é automatizada, reduzindo tanto o custo da geração e da manutenção quanto as falhas humanas. Desta forma, a aplicabilidade de métodos de geração de casos de teste baseados em modelos no contexto de sistemas embarcados vem sendo investigada. O objetivo deste trabalho de mestrado consiste em investigar a aplicabilidade dos métodos de geração em cenários de teste reais, com foco em sistemas embarcados, identificando as difi- culdades e limitações do processo, bem como os requisitos essenciais para a adequação dos métodos de geração propostos na literatura e de ferramentas de apoio à atividade de teste. O foco principal do projeto é a implementação de mecanismos que atendam aos requisitos levantados, visando a usabilidade, segurança e portabilidade da ferramenta / Test activities are essential to ensure the quality of products and identify faults to reduce maintenance costs and avoid that the client finds these faults. In this sense, model-based tests have been proved useful, because the cost of generating test cases and fault correction tend to be smaller. Due to its conceptual simplicity and expressiveness in describing the behavior of a system, Finite State Machines (FSM) have been used and researched in the model-based testing area. FSMs, employed with the support of appropriate tools, enable the generation of test cases in an automated way to assess the expected behavior of a system, reducing both the generation and maintenance costs and human failures. Thus, the applicability of test cases generation methods based on models in the context of embedded systems should be investigated. Test cases generation methods based on FSM are designed to derive test cases from the model. In this context, this work aims to investigate the applicability of generation methods in real-world scenarios, focusing embedded systems. It should identify the difficulties and limitations of the process, as well as the essential requirements for the adequacy of generation methods proposed in the literature and tools to support the test activity. The main focus of the project is the implementation of mechanisms that meet the elicited requirements in order to provide usability, security and tool portability

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-05-04T22:31:28Z No. of bitstreams: 1 ANA EMÍLIA VICTOR BARBOSA COUTINHO - TESE PPGCC 2015..pdf: 3805756 bytes, checksum: 2bee7d8777dfd753eb994680cd2bb6c5 (MD5) / Made available in DSpace on 2018-05-04T22:31:28Z (GMT). No. of bitstreams: 1 ANA EMÍLIA VICTOR BARBOSA COUTINHO - TESE PPGCC 2015..pdf: 3805756 bytes, checksum: 2bee7d8777dfd753eb994680cd2bb6c5 (MD5) Previous issue date: 2015-03-20 / Capes

A realização de atividades de teste é indispensável para a garantia da qualidade de um produto e para a identificação de defeitos, diminuindo custos de manutenção e evitando ao máximo o risco do cliente encontrar esses defeitos. Nessa linha, testes baseados em modelos têm se mostrado atrativos, pois o custo de geração de casos de testes e de correção de defeitos tende a ser menor. Devido à sua simplicidade conceitual e expressividade na descrição do comportamento de um sistema, um dos modelos mais usados e pesquisados na área de teste baseado em modelos são as Máquinas de Estados Finitos (MEFs). Por meio de MEFs e com apoio de ferramentas apropriadas, a geração de casos de testes para avaliar os comportamentos esperados de um sistema é automatizada, reduzindo tanto o custo da geração e da manutenção quanto as falhas humanas. Desta forma, a aplicabilidade de métodos de geração de casos de teste baseados em modelos no contexto de sistemas embarcados vem sendo investigada. O objetivo deste trabalho de mestrado consiste em investigar a aplicabilidade dos métodos de geração em cenários de teste reais, com foco em sistemas embarcados, identificando as difi- culdades e limitações do processo, bem como os requisitos essenciais para a adequação dos métodos de geração propostos na literatura e de ferramentas de apoio à atividade de teste. O foco principal do projeto é a implementação de mecanismos que atendam aos requisitos levantados, visando a usabilidade, segurança e portabilidade da ferramenta / Test activities are essential to ensure the quality of products and identify faults to reduce maintenance costs and avoid that the client finds these faults. In this sense, model-based tests have been proved useful, because the cost of generating test cases and fault correction tend to be smaller. Due to its conceptual simplicity and expressiveness in describing the behavior of a system, Finite State Machines (FSM) have been used and researched in the model-based testing area. FSMs, employed with the support of appropriate tools, enable the generation of test cases in an automated way to assess the expected behavior of a system, reducing both the generation and maintenance costs and human failures. Thus, the applicability of test cases generation methods based on models in the context of embedded systems should be investigated. Test cases generation methods based on FSM are designed to derive test cases from the model. In this context, this work aims to investigate the applicability of generation methods in real-world scenarios, focusing embedded systems. It should identify the difficulties and limitations of the process, as well as the essential requirements for the adequacy of generation methods proposed in the literature and tools to support the test activity. The main focus of the project is the implementation of mechanisms that meet the elicited requirements in order to provide usability, security and tool portability

Orientador: Arnaldo Vieira Moura / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T21:26:35Z (GMT). No. of bitstreams: 1 Pedrosa_LehiltonLelisChaves_M.pdf: 884292 bytes, checksum: e39efddad6809b28790b661469a5cfd2 (MD5) Previous issue date: 2010 / Resumo: Métodos formais são amplamente utilizados para modelar especificações e gerar casos de testes, imprescindíveis para validação de sistemas críticos. As Máquinas de Estados Finitos (MEFs) compõem um dos formalismos adotados, com várias aplicações em testes de sistemas aéreos e espaciais, além de sistemas médicos, entre vários outros. O objetivo de um método de geração automática de casos de testes é obter um conjunto de casos de testes, com o qual é possível verificar se uma dada implementação contém falhas. Um problema importante em métodos de geração de casos de teste com cobertura completa de falhas é o tamanho dos conjuntos de testes, que normalmente é exponencial no número de estados da MEF que está sendo testada. Para minimizar esse problema, diversas abordagens são adotadas, envolvendo melhorias nos métodos existentes, restrições do modelo de falhas e o uso de novas estratégias de teste. Esta dissertação estuda métodos automáticos para geração de casos de testes com cobertura completa de falhas e propõe dois novos métodos, que permitem reduzir o tamanho dos conjuntos de testes gerados. Primeiro, combinamos ideias do método Wp e do método G, visando usufruir as vantagens de ambos e obtendo um novo método, denominado Gp. Em seguida, descrevemos um novo modelo de falhas para sistemas compostos de vários subsistemas, possivelmente com um número alto de estados. Formalizamos tais sistemas, introduzindo o conceito de MEFs combinadas, e apresentamos um novo método de testes, denominado método C. Além disso, propomos uma abordagem de testes incremental, baseada no método C, que torna possível o teste de MEFs com um número arbitrário de estados. Estabelecemos comparações com abordagens tradicionais e mostramos que o uso da estratégia incremental pode gerar conjuntos de testes exponencialmente mais eficientes / Mestrado / Teoria da Computação / Mestre em Ciência da Computação

Orientador: Arnaldo Vieira Moura / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-15T05:28:23Z (GMT). No. of bitstreams: 1 Bonifacio_AdilsonLuiz_D.pdf: 1228504 bytes, checksum: 62db4b0286cfd1c735336e429629b3de (MD5) Previous issue date: 2009 / Resumo: O objetivo deste trabalho é prover métodos eficientes de geração de casos de teste para sistemas reativos críticos. Sistemas dessa natureza compreendem sistemas de tempo real e com transformações de contexto. Uma das técnicas mais usadas na geração de conjuntos de teste tem sido a abordagem baseada em modelos formais. Neste caso, os formalismos fornecem uma base sólida para que a atividade de teste seja efetuada de forma precisa e segura. Este trabalho propõe a construção de modelos formais, métodos e técnicas, bem como estratégias de teste, para dar suporte ao processo de geração automática de conjuntos de teste, aplicáveis a sistemas complexos. Porém, o processo de geração de testes baseado em modelos se torna, muitas vezes, impraticável em aplicações reais, devido ao problema da explosão combinatória de estados. Daí a necessidade de se encontrar modelos adequados que capturem o comportamento desejado dos sistemas a serem testados, bem como a importância de se construir métodos que contornem o problema da explosão do espaço de estado, de maneira razoável, permitindo que a geração de testes seja um processo aplicável a sistemas complexos. Entre os modelos abordados neste trabalho estão: (i) as tradicionais Máquinas de Estados Finito (FSM); (ii) uma extensão das FSMusando variáveis de contexto, as Máquinas de Estados Finito Estendida (EFSM); (iii) a extensão temporizada de EFSM (TEFSM), que possui, não apenas variáveis de contexto, mas também variáveis relógio; (iv) os modelos temporizados com entradas e saídas independentes, conhecidos como Timed I/O Automata (TIOA); e (v) uma extensão proposta para TIOA, denominado Timed I/O Context Automata (TIOCA), para compreender a evolução contínua de tempo e também as transformações de contexto. Com relação a geração de testes baseada em tais modelos, foi proposto, primeiramente, uma técnica de derivação de sequências de confirmação para TEFSM, usando model-checking. Em seguida, foi proposta uma generalização para um método de geração de conjuntos completos de teste usando FSM. Também foi desenvolvido um novo método de discretização do modelo TIOA, provendo a base necessária para a geração de casos de teste usando os conceitos de proposta de teste e produto síncrono. Por fim, foi desenvolvida uma extensão do método de discretização para TIOA também proposto neste trabalho, aplicado ao modelo TIOCA, permitindo a geração de testes em sistemas com evolução contínua de tempo e fluxo de dados, usando os conceitos de proposta de teste e produto de TIOCA / Abstract: This work aims to provide efficient test case generation methods for reactive and critical systems. In general, reactive and critical systems are real-time systems with context transformations. One of the most promising techniques for generating test suites is model-based testing. The formalisms supply the basis to perform a precise and dependable testing activity. In this scenery, our work proposes a construction of formal models, methods and techniques, as well as testing strategies, to support the process of automatically generating test suites for complex systems. However, the test generation process using formal models is usually infeasible in real applications, due to the state space explosion. Therefore, we need to find out suitable models to capture the system behaviors, and also to construct methods that can overcome the explosion problem, in a reasonable way, allowing the generation of test suites for complex systems. In this work we treat the following formal models: the conventional FSM; an extension of FSM using context variables (EFSM); the proposed extension of EFSM (TEFSM) to capture context variables and also clock variables; timed models, with disassociated input and output actions, called TIOA; and the proposed extension for TIOA, so-called TIOCA, to capture continuous time evolution and context transformations. In a first step of this work we proposed a technique to derive confirming sequences for TEFSM, using model-checking. Next, a classical method to generate complete test suites was generalized for FSM.We also proposed a new discretizationmethod for TIOA models, allowing the test case generation using test purpose and the synchronous product. Lastly, we extended the discretization method for TIOA to obtain more compact grid automata for TIOCA models, allowing the test case generation for systems with continuous time evolution and data flow transformations, using the notion of test purpose and the product of TIOCA / Doutorado / Teoria da Computação e Teste de Sistemas / Doutor em Ciência da Computação

Orientador: Eliane Martins / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-24T16:35:59Z (GMT). No. of bitstreams: 1 Letizio_CarolineCastello_M.pdf: 1670478 bytes, checksum: c2f330cd004addd705aef75384effcd2 (MD5) Previous issue date: 2013 / Resumo: Teste baseado em modelo é uma técnica na qual um sistema é modelado e geram-se testes a partir do modelo. Esta técnica apresenta como uma das maiores dificuldades a modelagem do sistema. Alguns dos empecilhos encontrados ao modelar são o que considerar do sistema e como representar essas considerações no modelo, incluindo em aplicações Web. Sendo assim, este trabalho propõe um método para auxiliar na modelagem de aplicações Web. Esta escolha é motivada pelo fato que esse tipo de sistema tem sido cada vez mais utilizado nos últimos anos e, com a sua evolução, sua complexidade tem aumentado consideravelmente, devido à dinamicidade e interatividade que esse tipo de aplicação oferece. A abordagem proposta é baseada em trabalhos correlatos, para se saber o que modelar da aplicação Web e como criar o modelo, descrevendo-se o passo-a-passo para se gerar os testes a partir dos modelos desenvolvidos e aplicá-los no sistema. A abordagem deste trabalho sugere tanto formas manuais como automáticas para os testes baseados em modelos. O método foi proposto para testar uma aplicação real: o ambiente de ensino à distância TelEduc. Os resultados, obtidos a partir da aplicação da proposta deste trabalho por um analista de teste e pela própria equipe do TelEduc, são analisados, a fim de validar a proposta e auxiliar no processo de desenvolvimento e aplicação dos testes de equipes de qualidade de software, principalmente, daquelas que não possuem nenhuma forma de organização de testes / Abstract: Model based testing is a technique in which the system is modeled and, from this model, tests can be generated. The major difficulty about this technique is to generate the model, since it is problematic to define what should be considered from the system and insert these characteristics into the model. This technique is also used in Web applications which presents the same challenges. Therefore, the present work proposes a method to assist in the modeling of Web applications. This sort of system has been increasingly used in recent years, where the system¿s complexity has considerably grown due to the dynamic and interactivity that this kind of application offers. The proposed method is based on related works in order to know what to model from the applications and how to create this model. The method contains the steps to generate tests cases from the created model, and how to execute them in the system. This work also suggests manual and automatic ways to execute the method. The proposal has been applied to test a real application: the e-learning Web environment TelEduc. The results obtained from the method¿s application by a test analyst and by the TelEduc team, are here analyzed to validate the method and to assist in the process development and tests execution by quality teams, especially those teams where there are no means of tests organization. / Mestrado / Ciência da Computação / Mestra em Ciência da Computação