Automatic test case generation for finite state machines

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 eficientesFormal methods are widely used to model specifications and to select test cases to validate critical systems. Finite State Machines (FSMs) are used as the basic formalism in several applications, such as those used in aerial, spacial, and medical systems. The goal of a test case generation method is to obtain a set of test cases, which can be used to check whether a given implementation is valid. For test methods with complete fault coverage, the size of the generated test suites is an important matter. This is a problematic issue, since the size of test suites is usually exponential on the number of states of the FSM under test. To minimize this problem, several different approaches were devised, such as the improvement of existing test methods, the adoption of restricted fault models, and the use of new testing strategies. Here, we study existing test case generation methods with complete fault coverage, and we introduce two new methods, that can reduce the size of the generated test suites. First, we combine ideas of the Wp-method and of the G-method. We combine advantages of both, and obtain a new method, named the Gp-method. Then, we describe a new fault model for systems composed of several subsystems, which may possibly contain a large number of states. We formalize such systems using the new concept of combined FSMs, and proceed to present a new test method, called the C-method. Starting with the C-method, we propose a new approach for incremental testing, that allows the test of FSMs with an arbitrary number of states. We compare this new strategy with traditional approaches, and we show that the use of the incremental testing strategy may generate test suites exponentially more efficient than those resulting from traditional approache